def mod2_double

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

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

345def mod2_double(+k: Nat) -> {Nat.mod(Nat.double(k), 2n) == 0n : Nat}:
346  +x = Nat.double(k)
347  +e1 = Equal.trans(Nat, x, Nat.add(Nat.double(Nat.div(x, 2n)), Nat.mod(x, 2n)), Nat.add(x, Nat.mod(x, 2n)), BT.half_eq(x), Equal.cong(Nat, Nat, t => Nat.add(Nat.double(t), Nat.mod(x, 2n)), Nat.div(x, 2n), k, N.div2_double(k)))
348  +e2 = Equal.cong(Nat, Nat, t => Nat.sub(t, x), Nat.add(x, Nat.mod(x, 2n)), x, Equal.sym(Nat, x, Nat.add(x, Nat.mod(x, 2n)), e1))
349  Equal.trans(Nat, Nat.mod(x, 2n), Nat.sub(Nat.add(x, Nat.mod(x, 2n)), x), 0n, Equal.sym(Nat, Nat.sub(Nat.add(x, Nat.mod(x, 2n)), x), Nat.mod(x, 2n), N.add_sub_cancel(x, Nat.mod(x, 2n))), Equal.trans(Nat, Nat.sub(Nat.add(x, Nat.mod(x, 2n)), x), Nat.sub(x, x), 0n, e2, N.sub_self(x)))