def odd_true

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

import Base

351def odd_true(+n: Nat, +h: {Nat.mod(n, 2n) == 1n : Nat}) -> {odd(n) == True{} : Bool}:
352  Equal.cong(Nat, Bool, t => Nat.is_eq(t, 1n), Nat.mod(n, 2n), 1n, h)