def odd_dvd_r

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

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

118# a divisor of an odd number is odd
119def odd_dvd_r(+a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +d: Nat, +ka: Nat, +ea: {a == Nat.mul(ka, d) : Nat}, +r: Nat, +hr: {Nat.mod(d, 2n) == r : Nat}) -> {Nat.mod(d, 2n) == 1n : Nat}:
120  match r:
121    case 0n:
122      +ed = even_form(d, hr)
123      +e1 = Equal.trans(Nat, a, Nat.mul(ka, d), Nat.mul(ka, Nat.double(Nat.div(d, 2n))), ea, Equal.cong(Nat, Nat, t => Nat.mul(ka, t), d, Nat.double(Nat.div(d, 2n)), ed))
124      +e2 = Equal.trans(Nat, Nat.mul(ka, Nat.double(Nat.div(d, 2n))), Nat.mul(Nat.double(Nat.div(d, 2n)), ka), Nat.double(Nat.mul(Nat.div(d, 2n), ka)), NA.mul_comm(ka, Nat.double(Nat.div(d, 2n))), dmul(Nat.div(d, 2n), ka))
125      +e3 = Equal.trans(Nat, Nat.double(Nat.mul(Nat.div(d, 2n), ka)), a, 1n+Nat.double(Nat.div(a, 2n)), Equal.sym(Nat, a, Nat.double(Nat.mul(Nat.div(d, 2n), ka)), Equal.trans(Nat, a, Nat.mul(ka, Nat.double(Nat.div(d, 2n))), Nat.double(Nat.mul(Nat.div(d, 2n), ka)), e1, e2)), odd_form(a, ha))
126      Empty.absurd({Nat.mod(d, 2n) == 1n : Nat}, N.even_odd(Nat.mul(Nat.div(d, 2n), ka), Nat.div(a, 2n), e3))
127    case 1n:
128      hr
129    case 2n+x:
130      Empty.absurd({Nat.mod(d, 2n) == 1n : Nat}, mod2_big(d, x, hr))