def strip_even

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

384# strip(2 (1 + kp)) <= 1 + kp
385def strip_even(+kp: Nat) -> {Nat.is_le(nstrip(Nat.double(1n+kp)), 1n+kp) == True{} : Bool}:
386  +eo = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 1n), Nat.mod(Nat.double(1n+kp), 2n), 0n, mod2_double(1n+kp))
387  %Equal.sym(Nat, nstrip_go(140n, Nat.double(1n+kp), odd(Nat.double(1n+kp))), nstrip_go(140n, Nat.double(1n+kp), False{}), Equal.cong(Bool, Nat, t => nstrip_go(140n, Nat.double(1n+kp), t), odd(Nat.double(1n+kp)), False{}, eo)) : {Nat.is_le(_, 1n+kp) == True{} : Bool}
388  %Equal.sym(Nat, Nat.div(Nat.double(1n+kp), 2n), 1n+kp, N.div2_double(1n+kp)) : {Nat.is_le(nstrip_go(139n, _, odd(_)), 1n+kp) == True{} : Bool}
389  strip_le(139n, 1n+kp, odd(1n+kp))