Bgcdnat.bfirst: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as Bgcdnat
Lines 480-487 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&start_line=480&end_line=487

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/math/natural/roots.bend as RT

# a odd, b > 0, a b < 2^139: the loop computes gcd(a, b)
def bfirst(+a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +bp: Nat, +hab: {Nat.is_lt(Nat.mul(a, 1n+bp), C.pow2(139n)) == True{} : Bool}) -> {nbloop(140n, a, 1n+bp, iz(1n+bp), nsm(a, 1n+bp)) == M.gcd(a, 1n+bp) : Nat}:
  +k1 = N.le_trans(1n+bp, Nat.mul(1n+bp, a), Nat.mul(a, 1n+bp), RT.le_mul_pos(1n+bp, a, odd_pos(a, ha)), N.eq_le(Nat.mul(1n+bp, a), Nat.mul(a, 1n+bp), NA.mul_comm(1n+bp, a)))
  +k2 = N.lt_le_trans(1n+bp, C.pow2(139n), C.pow2(140n), N.le_lt_trans(1n+bp, Nat.mul(a, 1n+bp), C.pow2(139n), k1, hab), N.pow2_mono(139n, 140n, {==}))
  +hs = odd_eq(nstrip(1n+bp), strip_odd(140n, 1n+bp, {==}, k2, odd(1n+bp), {==}))
  +hga = Equal.sym(Nat, M.gcd(a, nstrip(1n+bp)), M.gcd(a, 1n+bp), strip_gcd(a, ha, 140n, 1n+bp, odd(1n+bp), {==}))
  +hsa = NF.mul_le_r(a, nstrip(1n+bp), 1n+bp, strip_le(140n, 1n+bp, odd(1n+bp)))
  bf_sm(a, bp, nsm(a, 1n+bp), bf_case(a, ha, bp, hab, hs, hga, hsa, Nat.is_lt(nstrip(1n+bp), a), {==}))

Uses (28):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=eq_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=pow2_mono
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend&name=le_mul_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=bf_case
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=bf_sm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=iz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=nbloop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=nsm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=nstrip
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=odd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=odd_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=odd_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=strip_gcd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=strip_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend&name=strip_odd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=mul_le_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=gcd