def odd_sub

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

import Base

362# odd a - odd s is even
363def odd_sub(+a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +s: Nat, +hs: {Nat.mod(s, 2n) == 1n : Nat}) -> {Nat.sub(a, s) == Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(s, 2n))) : Nat}:
364  %Equal.sym(Nat, a, 1n+Nat.double(Nat.div(a, 2n)), odd_form(a, ha)) : {Nat.sub(_, s) == Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(s, 2n))) : Nat}
365  %Equal.sym(Nat, s, 1n+Nat.double(Nat.div(s, 2n)), odd_form(s, hs)) : {Nat.sub(1n+Nat.double(Nat.div(a, 2n)), _) == Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(s, 2n))) : Nat}
366  double_sub(Nat.div(a, 2n), Nat.div(s, 2n))