def odd_pos

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

import Base

354def odd_pos(+n: Nat, +h: {Nat.mod(n, 2n) == 1n : Nat}) -> {Nat.is_lt(0n, n) == True{} : Bool}:
355  %Equal.sym(Nat, n, 1n+Nat.double(Nat.div(n, 2n)), odd_form(n, h)) : {Nat.is_lt(0n, _) == True{} : Bool}
356  {==}