n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ ↑(gcdAux n (b % pos a) (pos a)) = Nat.gcd ↑a ↑b
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ ↑(gcdAux (Nat.succ n) (pos a) b) = Nat.gcd ↑(pos a) ↑b
simp [gcdAux]
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ Nat.gcd (↑b % ↑(pos a)) ↑(pos a) = Nat.gcd (↑b % ↑a) ↑a

case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ b % pos a ≤ pos a

case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ natSize (b % pos a * pos a) ≤ n
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ ↑(gcdAux n (b % pos a) (pos a)) = Nat.gcd ↑a ↑b
rw [Nat.gcd_rec, gcd_to_nat_aux, mod_to_nat]
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * ↑b < 2 ^ Nat.succ n
⊢ ↑(b % pos a) * ↑(pos a) < 2 ^ n
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ natSize (b % pos a * pos a) ≤ n
rw [natSize_to_nat, mul_to_nat, Nat.size_le] at h⊢
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * ↑b < 2 ^ Nat.succ n
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * ↑b < 2 ^ Nat.succ n
⊢ ↑(b % pos a) * ↑(pos a) < 2 ^ n
rw [mod_to_nat, mul_comm]
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * ↑b < 2 ^ Nat.succ n
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
rw [pow_succ', ← Nat.mod_add_div b (pos a)] at h
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) * 2 ≤ ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a)))
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
refine' lt_of_mul_lt_mul_right (lt_of_le_of_lt _ h) (Nat.zero_le 2)
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑b % ↑(pos a)) ≤
    ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑(pos a) * (↑b / ↑(pos a)))
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) * 2 ≤ ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a)))
rw [mul_two, mul_add]
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑a ≤ ↑(pos a) * (↑b / ↑(pos a))
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑b % ↑(pos a)) ≤
    ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑(pos a) * (↑b / ↑(pos a)))
refine'
  add_le_add_left
    (Nat.mul_le_mul_left _ (le_trans (le_of_lt (Nat.mod_lt _ (PosNum.cast_pos _))) _)) _
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
this : 1 ≤ ?m.1170277
⊢ ↑a ≤ ↑(pos a) * (↑b / ↑(pos a))

case this
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 1 ≤ ?m.1170277
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑a ≤ ↑(pos a) * (↑b / ↑(pos a))
suffices : 1 ≤ _
case this
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 1 ≤ ↑b / ↑a
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
this : 1 ≤ ?m.1170277
⊢ ↑a ≤ ↑(pos a) * (↑b / ↑(pos a))

case this
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 1 ≤ ?m.1170277
simpa using Nat.mul_le_mul_left (pos a) this
case this
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑a ≤ ↑b
case this
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 1 ≤ ↑b / ↑a
rw [Nat.le_div_iff_mul_le a.cast_pos, one_mul]
no goals
case this
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑a ≤ ↑b
exact le_to_nat.2 ab
no goals
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ Nat.gcd (↑b % ↑(pos a)) ↑(pos a) = Nat.gcd (↑b % ↑a) ↑a
rfl
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ ↑b % ↑(pos a) ≤ ↑(pos a)
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ b % pos a ≤ pos a
rw [← le_to_nat, mod_to_nat]
no goals
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : natSize (pos a * b) ≤ Nat.succ n
⊢ ↑b % ↑(pos a) ≤ ↑(pos a)
exact le_of_lt (Nat.mod_lt _ (PosNum.cast_pos _))