def odd2_m

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

132# an odd d dividing 2 m divides m
133def odd2_m(+m: Nat, +d: Nat, +hd: {Nat.mod(d, 2n) == 1n : Nat}, +kb: Nat, +eb: {Nat.double(m) == Nat.mul(kb, d) : Nat}, +r: Nat, +hr: {Nat.mod(kb, 2n) == r : Nat}) -> S.dvd(d, m):
134  match r:
135    case 0n:
136      +q = Nat.div(kb, 2n)
137      +ek = even_form(kb, hr)
138      +e1 = Equal.trans(Nat, Nat.double(m), Nat.mul(kb, d), Nat.double(Nat.mul(q, d)), eb, Equal.trans(Nat, Nat.mul(kb, d), Nat.mul(Nat.double(q), d), Nat.double(Nat.mul(q, d)), Equal.cong(Nat, Nat, t => Nat.mul(t, d), kb, Nat.double(q), ek), dmul(q, d)))
139      (q, N.double_inj(m, Nat.mul(q, d), e1))
140    case 1n:
141      +q = Nat.div(kb, 2n)
142      +p = Nat.div(d, 2n)
143      +ek = odd_form(kb, hr)
144      +ed = odd_form(d, hd)
145      +e1 = Equal.trans(Nat, Nat.double(m), Nat.mul(kb, d), Nat.mul(1n+Nat.double(q), d), eb, Equal.cong(Nat, Nat, t => Nat.mul(t, d), kb, 1n+Nat.double(q), ek))
146      +e2 = Equal.cong(Nat, Nat, t => Nat.add(d, t), Nat.mul(Nat.double(q), d), Nat.double(Nat.mul(q, d)), dmul(q, d))
147      +e3 = Equal.cong(Nat, Nat, t => Nat.add(t, Nat.double(Nat.mul(q, d))), d, 1n+Nat.double(p), ed)
148      +e4 = N.add_double(p, Nat.mul(q, d))
149      +e5 = Equal.trans(Nat, Nat.double(m), Nat.add(d, Nat.double(Nat.mul(q, d))), 1n+Nat.double(Nat.add(p, Nat.mul(q, d))), Equal.trans(Nat, Nat.double(m), Nat.mul(1n+Nat.double(q), d), Nat.add(d, Nat.double(Nat.mul(q, d))), e1, e2), Equal.trans(Nat, Nat.add(d, Nat.double(Nat.mul(q, d))), 1n+Nat.add(Nat.double(p), Nat.double(Nat.mul(q, d))), 1n+Nat.double(Nat.add(p, Nat.mul(q, d))), e3, N.succ_cong(Nat.add(Nat.double(p), Nat.double(Nat.mul(q, d))), Nat.double(Nat.add(p, Nat.mul(q, d))), e4)))
150      Empty.absurd(S.dvd(d, m), N.even_odd(m, Nat.add(p, Nat.mul(q, d)), e5))
151    case 2n+x:
152      Empty.absurd(S.dvd(d, m), mod2_big(kb, x, hr))