def div_one
bend-collections-laws-math@1.0.0.0 · proofs/math/random/lemire.bend:461
import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as Lemire
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as AR
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
461def div_one(+N: Nat) -> {Nat.div(N, 1n) == N : Nat}:
462 %Equal.sym(Nat, N, Nat.add(Nat.mul(N, 1n), 0n), Equal.trans(Nat, N, Nat.mul(N, 1n), Nat.add(Nat.mul(N, 1n), 0n), Equal.sym(Nat, Nat.mul(N, 1n), N, NA.mul_one(N)), Equal.sym(Nat, Nat.add(Nat.mul(N, 1n), 0n), Nat.mul(N, 1n), N.add_zero(Nat.mul(N, 1n))))) : {Nat.div(_, 1n) == N : Nat}
463 AR.div_of(N, 0n, 0n, {==})