def not_odd_r

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

262# not odd is even
263def not_odd_r(+n: Nat, +h: {odd(n) == False{} : Bool}, +r: Nat, +hr: {Nat.mod(n, 2n) == r : Nat}) -> {Nat.mod(n, 2n) == 0n : Nat}:
264  match r:
265    case 0n:
266      hr
267    case 1n:
268      +e = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 1n), Nat.mod(n, 2n), 1n, hr)
269      Empty.absurd({Nat.mod(n, 2n) == 0n : Nat}, NF.true_ne_false(Equal.trans(Bool, True{}, odd(n), False{}, Equal.sym(Bool, odd(n), True{}, e), h)))
270    case 2n+x:
271      Empty.absurd({Nat.mod(n, 2n) == 0n : Nat}, mod2_big(n, x, hr))