def mod2_big

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

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

113# n mod 2 is 0 or 1
114def mod2_big(+n: Nat, +x: Nat, +hr: {Nat.mod(n, 2n) == 2n+x : Nat}) -> Empty:
115  +c = Equal.cong(Nat, Bool, t => Nat.is_lt(t, 2n), Nat.mod(n, 2n), 2n+x, hr)
116  N.lt_zero_absurd(x, Equal.trans(Bool, Nat.is_lt(2n+x, 2n), Nat.is_lt(Nat.mod(n, 2n), 2n), True{}, Equal.sym(Bool, Nat.is_lt(Nat.mod(n, 2n), 2n), Nat.is_lt(2n+x, 2n), c), BT.half_rem(n)))