def bl_case
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:391
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as Bgcdnat
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
391def bl_case(+g: Nat, +a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +kp: Nat, +hbg: {Nat.is_lt(Nat.mul(a, 1n+kp), C.pow2(g)) == True{} : Bool}, ih: @+a2: Nat -> @+ha2: {Nat.mod(a2, 2n) == 1n : Nat} -> @+k2: Nat -> @+hb2: {Nat.is_lt(Nat.mul(a2, Nat.double(k2)), C.pow2(g)) == True{} : Bool} -> {nbloop(g, a2, Nat.double(k2), iz(Nat.double(k2)), nsm(a2, Nat.double(k2))) == M.gcd(a2, Nat.double(k2)) : Nat}, +hs: {Nat.mod(nstrip(Nat.double(1n+kp)), 2n) == 1n : Nat}, +hsle: {Nat.is_le(nstrip(Nat.double(1n+kp)), 1n+kp) == True{} : Bool}, +hga: {M.gcd(a, Nat.double(1n+kp)) == M.gcd(a, nstrip(Nat.double(1n+kp))) : Nat}, +hsa: {Nat.is_le(Nat.mul(a, nstrip(Nat.double(1n+kp))), Nat.mul(a, 1n+kp)) == True{} : Bool}, +lb: Bool, +hl: {Nat.is_lt(nstrip(Nat.double(1n+kp)), a) == lb : Bool}) -> {nbloop(g, nba(a, nstrip(Nat.double(1n+kp)), lb), nbd(a, nstrip(Nat.double(1n+kp)), lb), iz(nbd(a, nstrip(Nat.double(1n+kp)), lb)), nsm(nba(a, nstrip(Nat.double(1n+kp)), lb), nbd(a, nstrip(Nat.double(1n+kp)), lb))) == M.gcd(a, Nat.double(1n+kp)) : Nat}:
392 match lb:
393 case True{}:
394 +sle = N.lt_le(nstrip(Nat.double(1n+kp)), a, hl)
395 +le1 = N.le_trans(Nat.mul(nstrip(Nat.double(1n+kp)), Nat.sub(a, nstrip(Nat.double(1n+kp)))), Nat.mul(nstrip(Nat.double(1n+kp)), a), Nat.mul(a, 1n+kp), NF.mul_le_r(nstrip(Nat.double(1n+kp)), Nat.sub(a, nstrip(Nat.double(1n+kp))), a, UH.sub_le(a, nstrip(Nat.double(1n+kp)))), N.le_trans(Nat.mul(nstrip(Nat.double(1n+kp)), a), Nat.mul(a, nstrip(Nat.double(1n+kp))), Nat.mul(a, 1n+kp), N.eq_le(Nat.mul(nstrip(Nat.double(1n+kp)), a), Nat.mul(a, nstrip(Nat.double(1n+kp))), NA.mul_comm(nstrip(Nat.double(1n+kp)), a)), hsa))
396 +hDs = Equal.sym(Nat, Nat.sub(a, nstrip(Nat.double(1n+kp))), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n))), odd_sub(a, ha, nstrip(Nat.double(1n+kp)), hs))
397 +hb2 = Equal.trans(Bool, Nat.is_lt(Nat.mul(nstrip(Nat.double(1n+kp)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n)))), C.pow2(g)), Nat.is_lt(Nat.mul(nstrip(Nat.double(1n+kp)), Nat.sub(a, nstrip(Nat.double(1n+kp)))), C.pow2(g)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(Nat.mul(nstrip(Nat.double(1n+kp)), t), C.pow2(g)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n))), Nat.sub(a, nstrip(Nat.double(1n+kp))), hDs), N.le_lt_trans(Nat.mul(nstrip(Nat.double(1n+kp)), Nat.sub(a, nstrip(Nat.double(1n+kp)))), Nat.mul(a, 1n+kp), C.pow2(g), le1, hbg))
398 +r = ih(nstrip(Nat.double(1n+kp)), hs, Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n)), hb2)
399 %hDs : {nbloop(g, nstrip(Nat.double(1n+kp)), _, iz(_), nsm(nstrip(Nat.double(1n+kp)), _)) == M.gcd(a, Nat.double(1n+kp)) : Nat}
400 Equal.trans(Nat, nbloop(g, nstrip(Nat.double(1n+kp)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n))), iz(Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n)))), nsm(nstrip(Nat.double(1n+kp)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n))))), M.gcd(nstrip(Nat.double(1n+kp)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n)))), M.gcd(a, Nat.double(1n+kp)), r, Equal.trans(Nat, M.gcd(nstrip(Nat.double(1n+kp)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n)))), M.gcd(nstrip(Nat.double(1n+kp)), Nat.sub(a, nstrip(Nat.double(1n+kp)))), M.gcd(a, Nat.double(1n+kp)), Equal.cong(Nat, Nat, t => M.gcd(nstrip(Nat.double(1n+kp)), t), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(Nat.double(1n+kp)), 2n))), Nat.sub(a, nstrip(Nat.double(1n+kp))), hDs), Equal.trans(Nat, M.gcd(nstrip(Nat.double(1n+kp)), Nat.sub(a, nstrip(Nat.double(1n+kp)))), M.gcd(nstrip(Nat.double(1n+kp)), a), M.gcd(a, Nat.double(1n+kp)), Equal.sym(Nat, M.gcd(nstrip(Nat.double(1n+kp)), a), M.gcd(nstrip(Nat.double(1n+kp)), Nat.sub(a, nstrip(Nat.double(1n+kp)))), gcd_sub(nstrip(Nat.double(1n+kp)), a, sle)), Equal.trans(Nat, M.gcd(nstrip(Nat.double(1n+kp)), a), M.gcd(a, nstrip(Nat.double(1n+kp))), M.gcd(a, Nat.double(1n+kp)), gcd_comm(nstrip(Nat.double(1n+kp)), a), Equal.sym(Nat, M.gcd(a, Nat.double(1n+kp)), M.gcd(a, nstrip(Nat.double(1n+kp))), hga)))))
401 case False{}:
402 +ale = N.not_lt_le(nstrip(Nat.double(1n+kp)), a, hl)
403 +le1 = N.le_trans(Nat.mul(a, Nat.sub(nstrip(Nat.double(1n+kp)), a)), Nat.mul(a, nstrip(Nat.double(1n+kp))), Nat.mul(a, 1n+kp), NF.mul_le_r(a, Nat.sub(nstrip(Nat.double(1n+kp)), a), nstrip(Nat.double(1n+kp)), UH.sub_le(nstrip(Nat.double(1n+kp)), a)), hsa)
404 +hDs = Equal.sym(Nat, Nat.sub(nstrip(Nat.double(1n+kp)), a), Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n))), odd_sub(nstrip(Nat.double(1n+kp)), hs, a, ha))
405 +hb2 = Equal.trans(Bool, Nat.is_lt(Nat.mul(a, Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n)))), C.pow2(g)), Nat.is_lt(Nat.mul(a, Nat.sub(nstrip(Nat.double(1n+kp)), a)), C.pow2(g)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(Nat.mul(a, t), C.pow2(g)), Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n))), Nat.sub(nstrip(Nat.double(1n+kp)), a), hDs), N.le_lt_trans(Nat.mul(a, Nat.sub(nstrip(Nat.double(1n+kp)), a)), Nat.mul(a, 1n+kp), C.pow2(g), le1, hbg))
406 +r = ih(a, ha, Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n)), hb2)
407 %hDs : {nbloop(g, a, _, iz(_), nsm(a, _)) == M.gcd(a, Nat.double(1n+kp)) : Nat}
408 Equal.trans(Nat, nbloop(g, a, Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n))), iz(Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n)))), nsm(a, Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n))))), M.gcd(a, Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n)))), M.gcd(a, Nat.double(1n+kp)), r, Equal.trans(Nat, M.gcd(a, Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n)))), M.gcd(a, Nat.sub(nstrip(Nat.double(1n+kp)), a)), M.gcd(a, Nat.double(1n+kp)), Equal.cong(Nat, Nat, t => M.gcd(a, t), Nat.double(Nat.sub(Nat.div(nstrip(Nat.double(1n+kp)), 2n), Nat.div(a, 2n))), Nat.sub(nstrip(Nat.double(1n+kp)), a), hDs), Equal.trans(Nat, M.gcd(a, Nat.sub(nstrip(Nat.double(1n+kp)), a)), M.gcd(a, nstrip(Nat.double(1n+kp))), M.gcd(a, Nat.double(1n+kp)), Equal.sym(Nat, M.gcd(a, nstrip(Nat.double(1n+kp))), M.gcd(a, Nat.sub(nstrip(Nat.double(1n+kp)), a)), gcd_sub(a, nstrip(Nat.double(1n+kp)), ale)), Equal.sym(Nat, M.gcd(a, Nat.double(1n+kp)), M.gcd(a, nstrip(Nat.double(1n+kp))), hga))))