def prime_of
bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:80
import bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend as Fixprime
import Base
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB
import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as PR
80def prime_of(+m: U32, +pr: Bool, +hpr: {NB.is_prime(v(m)) == pr : Bool}) -> {SN.prime(v(m)) == pr : Bool}:
81 Equal.trans(Bool, SN.prime(v(m)), NB.is_prime(v(m)), pr, Equal.sym(Bool, NB.is_prime(v(m)), SN.prime(v(m)), PR.is_prime_value(v(m))), hpr)