def odd_form

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:106

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/bits.bend as BT

106def odd_form(+n: Nat, +h: {Nat.mod(n, 2n) == 1n : Nat}) -> {n == 1n+Nat.double(Nat.div(n, 2n)) : Nat}:
107  +e = Equal.cong(Nat, Nat, t => Nat.add(Nat.double(Nat.div(n, 2n)), t), Nat.mod(n, 2n), 1n, h)
108  Equal.trans(Nat, n, Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)), 1n+Nat.double(Nat.div(n, 2n)), BT.half_eq(n), Equal.trans(Nat, Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)), Nat.add(Nat.double(Nat.div(n, 2n)), 1n), 1n+Nat.double(Nat.div(n, 2n)), e, N.add_comm(Nat.double(Nat.div(n, 2n)), 1n)))