Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2018 Guy Leroy. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sangwoo Jo (aka Jason), Guy Leroy, Johannes HΓΆlzl, Mario Carneiro

! This file was ported from Lean 3 source module data.int.gcd
! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Algebra.GroupPower.Lemmas
import Mathlib.Algebra.Ring.Regular
import Mathlib.Data.Int.Dvd.Basic
import Mathlib.Order.Bounds.Basic

/-!
# Extended GCD and divisibility over β„€

## Main definitions

* Given `x y : β„•`, `xgcd x y` computes the pair of integers `(a, b)` such that
  `gcd x y = x * a + y * b`. `gcd_a x y` and `gcd_b x y` are defined to be `a` and `b`,
  respectively.

## Main statements

* `gcd_eq_gcd_ab`: BΓ©zout's lemma, given `x y : β„•`, `gcd x y = x * gcd_a x y + y * gcd_b x y`.

## Tags

BΓ©zout's lemma, Bezout's lemma
-/


/-! ### Extended Euclidean algorithm -/


namespace Nat

/-- Helper function for the extended GCD algorithm (`Nat.xgcd`). -/
def 
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux : 
β„•: Type
β„• β†’ 
β„€: Type
β„€ β†’ 
β„€: Type
β„€ β†’ 
β„•: Type
β„• β†’ 
β„€: Type
β„€ β†’ 
β„€: Type
β„€ β†’ 
β„•: Type
β„• Γ— 
β„€: Type
β„€ Γ— 
β„€: Type
β„€
  | 
0: β„•
0, _, _, 
r': β„•
r', 
s': β„€
s', 
t': β„€
t' => (
r': β„•
r', 
s': β„€
s', 
t': β„€
t')
  | 
succ: β„• β†’ β„•
succ 
k: β„•
k, 
s: β„€
s, 
t: β„€
t, 
r': β„•
r', 
s': β„€
s', 
t': β„€
t' =>
    have : 
r': β„•
r' % 
succ: β„• β†’ β„•
succ 
k: β„•
k < 
succ: β„• β†’ β„•
succ 
k: β„•
k := 
mod_lt: βˆ€ (x : β„•) {y : β„•}, y > 0 β†’ x % y < y
mod_lt 
_: β„•
_ <| (
succ_pos: βˆ€ (n : β„•), 0 < succ n
succ_pos 
_: β„•
_).
gt: βˆ€ {Ξ± : Type ?u.212} [inst : LT Ξ±] {x y : Ξ±}, x < y β†’ y > x
gt
    let 
q: ?m.228
q := 
r': β„•
r' / 
succ: β„• β†’ β„•
succ 
k: β„•
k
    
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux (
r': β„•
r' % 
succ: β„• β†’ β„•
succ 
k: β„•
k) (
s': β„€
s' - 
q: ?m.228
q * 
s: β„€
s) (
t': β„€
t' - 
q: ?m.228
q * 
t: β„€
t) (
succ: β„• β†’ β„•
succ 
k: β„•
k) 
s: β„€
s 
t: β„€
t
#align nat.xgcd_aux 
Nat.xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
Nat.xgcdAux

-- porting note: these are not in mathlib3; these equation lemmas are to fix
-- complaints by the Lean 4 `unusedHavesSuffices` linter obtained when `simp [xgcdAux]` is used.
theorem 
xgcdAux_zero: βˆ€ {s t : β„€} {r' : β„•} {s' t' : β„€}, xgcdAux 0 s t r' s' t' = (r', s', t')
xgcdAux_zero : 
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux 
0: ?m.12476
0 
s: ?m.12439
s 
t: ?m.12447
t 
r': ?m.12455
r' 
s': ?m.12463
s' 
t': ?m.12471
t' = (
r': ?m.12455
r', 
s': ?m.12463
s', 
t': ?m.12471
t') := 
rfl: βˆ€ {Ξ± : Sort ?u.12495} {a : Ξ±}, a = a
rfl

theorem 
xgcdAux_succ: βˆ€ {k : β„•} {s t : β„€} {r' : β„•} {s' t' : β„€},
  xgcdAux (succ k) s t r' s' t' =     xgcdAux (r' % succ k) (s' - ↑r' / ↑(succ k) * s) (t' - ↑r' / ↑(succ k) * t) (succ k) s t
xgcdAux_succ : 
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux (
succ: β„• β†’ β„•
succ 
k: ?m.12522
k) 
s: ?m.12527
s 
t: ?m.12532
t 
r': ?m.12537
r' 
s': ?m.12542
s' 
t': ?m.12547
t' =
  
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux (
r': ?m.12537
r' % 
succ: β„• β†’ β„•
succ 
k: ?m.12522
k) (
s': ?m.12542
s' - (
r': ?m.12537
r' / 
succ: β„• β†’ β„•
succ 
k: ?m.12522
k) * 
s: ?m.12527
s) (
t': ?m.12547
t' - (
r': ?m.12537
r' / 
succ: β„• β†’ β„•
succ 
k: ?m.12522
k) * 
t: ?m.12532
t) (
succ: β„• β†’ β„•
succ 
k: ?m.12522
k) 
s: ?m.12527
s 
t: ?m.12532
t := 
rfl: βˆ€ {Ξ± : Sort ?u.13002} {a : Ξ±}, a = a
rfl

@[simp]
theorem 
xgcd_zero_left: βˆ€ {s t : β„€} {r' : β„•} {s' t' : β„€}, xgcdAux 0 s t r' s' t' = (r', s', t')
xgcd_zero_left {
s: ?m.13170
s 
t: ?m.13173
t 
r': ?m.13176
r' 
s': ?m.13179
s' 
t': ?m.13182
t'} : 
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux 
0: ?m.13187
0 
s: ?m.13170
s 
t: ?m.13173
t 
r': ?m.13176
r' 
s': ?m.13179
s' 
t': ?m.13182
t' = (
r': ?m.13176
r', 
s': ?m.13179
s', 
t': ?m.13182
t') := 
Goals accomplished! πŸ™
s, t: β„€

r': β„•

s', t': β„€

xgcdAux 0 s t r' s' t' = (r', s', t')
Goals accomplished! πŸ™

#align nat.xgcd_zero_left 
Nat.xgcd_zero_left: βˆ€ {s t : β„€} {r' : β„•} {s' t' : β„€}, xgcdAux 0 s t r' s' t' = (r', s', t')
Nat.xgcd_zero_left

theorem 
xgcd_aux_rec: βˆ€ {r : β„•} {s t : β„€} {r' : β„•} {s' t' : β„€},
  0 < r β†’ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
xgcd_aux_rec {
r: ?m.14182
r 
s: β„€
s 
t: β„€
t 
r': ?m.14191
r' 
s': β„€
s' 
t': β„€
t'} (
h: 0 < r
h : 
0: ?m.14202
0 < 
r: ?m.14182
r) :
    
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux 
r: ?m.14182
r 
s: ?m.14185
s 
t: ?m.14188
t 
r': ?m.14191
r' 
s': ?m.14194
s' 
t': ?m.14197
t' = 
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux (
r': ?m.14191
r' % 
r: ?m.14182
r) (
s': ?m.14194
s' - 
r': ?m.14191
r' / 
r: ?m.14182
r * 
s: ?m.14185
s) (
t': ?m.14197
t' - 
r': ?m.14191
r' / 
r: ?m.14182
r * 
t: ?m.14188
t) 
r: ?m.14182
r 
s: ?m.14185
s 
t: ?m.14188
t := 
Goals accomplished! πŸ™
r: β„•

s, t: β„€

r': β„•

s', t': β„€

h: 0 < r

xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
s, t: β„€

r': β„•

s', t': β„€

r: β„•

h: 0 < succ r

intro
xgcdAux (succ r) s t r' s' t' = xgcdAux (r' % succ r) (s' - ↑r' / ↑(succ r) * s) (t' - ↑r' / ↑(succ r) * t) (succ r) s t
r: β„•

s, t: β„€

r': β„•

s', t': β„€

h: 0 < r

xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
Goals accomplished! πŸ™

#align nat.xgcd_aux_rec 
Nat.xgcd_aux_rec: βˆ€ {r : β„•} {s t : β„€} {r' : β„•} {s' t' : β„€},
  0 < r β†’ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
Nat.xgcd_aux_rec

/-- Use the extended GCD algorithm to generate the `a` and `b` values
  satisfying `gcd x y = x * a + y * b`. -/
def 
xgcd: β„• β†’ β„• β†’ β„€ Γ— β„€
xgcd (
x: β„•
x 
y: β„•
y : 
β„•: Type
β„•) : 
β„€: Type
β„€ Γ— 
β„€: Type
β„€ :=
  (
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux 
x: β„•
x 
1: ?m.14990
1 
0: ?m.15001
0 
y: β„•
y 
0: ?m.15008
0 
1: ?m.15011
1).
2: {Ξ± : Type ?u.15014} β†’ {Ξ² : Type ?u.15013} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2
#align nat.xgcd 
Nat.xgcd: β„• β†’ β„• β†’ β„€ Γ— β„€
Nat.xgcd

/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
def 
gcdA: β„• β†’ β„• β†’ β„€
gcdA (
x: β„•
x 
y: β„•
y : 
β„•: Type
β„•) : 
β„€: Type
β„€ :=
  (
xgcd: β„• β†’ β„• β†’ β„€ Γ— β„€
xgcd 
x: β„•
x 
y: β„•
y).
1: {Ξ± : Type ?u.15082} β†’ {Ξ² : Type ?u.15081} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1
#align nat.gcd_a 
Nat.gcdA: β„• β†’ β„• β†’ β„€
Nat.gcdA

/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
def 
gcdB: β„• β†’ β„• β†’ β„€
gcdB (
x: β„•
x 
y: β„•
y : 
β„•: Type
β„•) : 
β„€: Type
β„€ :=
  (
xgcd: β„• β†’ β„• β†’ β„€ Γ— β„€
xgcd 
x: β„•
x 
y: β„•
y).
2: {Ξ± : Type ?u.15125} β†’ {Ξ² : Type ?u.15124} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2
#align nat.gcd_b 
Nat.gcdB: β„• β†’ β„• β†’ β„€
Nat.gcdB

@[simp]
theorem 
gcdA_zero_left: βˆ€ {s : β„•}, gcdA 0 s = 0
gcdA_zero_left {
s: β„•
s : 
β„•: Type
β„•} : 
gcdA: β„• β†’ β„• β†’ β„€
gcdA 
0: ?m.15164
0 
s: β„•
s = 
0: ?m.15175
0 := 
Goals accomplished! πŸ™
s: β„•

gcdA 0 s = 0
s: β„•

(xgcd 0 s).fst = 0
s: β„•

gcdA 0 s = 0
s: β„•

(xgcd 0 s).fst = 0
s: β„•

(xgcdAux 0 1 0 s 0 1).snd.fst = 0
s: β„•

(xgcd 0 s).fst = 0
s: β„•

(s, 0, 1).snd.fst = 0
Goals accomplished! πŸ™

#align nat.gcd_a_zero_left 
Nat.gcdA_zero_left: βˆ€ {s : β„•}, gcdA 0 s = 0
Nat.gcdA_zero_left

@[simp]
theorem 
gcdB_zero_left: βˆ€ {s : β„•}, gcdB 0 s = 1
gcdB_zero_left {
s: β„•
s : 
β„•: Type
β„•} : 
gcdB: β„• β†’ β„• β†’ β„€
gcdB 
0: ?m.15244
0 
s: β„•
s = 
1: ?m.15255
1 := 
Goals accomplished! πŸ™
s: β„•

gcdB 0 s = 1
s: β„•

(xgcd 0 s).snd = 1
s: β„•

gcdB 0 s = 1
s: β„•

(xgcd 0 s).snd = 1
s: β„•

(xgcdAux 0 1 0 s 0 1).snd.snd = 1
s: β„•

(xgcd 0 s).snd = 1
s: β„•

(s, 0, 1).snd.snd = 1
Goals accomplished! πŸ™

#align nat.gcd_b_zero_left 
Nat.gcdB_zero_left: βˆ€ {s : β„•}, gcdB 0 s = 1
Nat.gcdB_zero_left

@[simp]
theorem 
gcdA_zero_right: βˆ€ {s : β„•}, s β‰  0 β†’ gcdA s 0 = 1
gcdA_zero_right {
s: β„•
s : 
β„•: Type
β„•} (
h: s β‰  0
h : 
s: β„•
s β‰  
0: ?m.15323
0) : 
gcdA: β„• β†’ β„• β†’ β„€
gcdA 
s: β„•
s 
0: ?m.15337
0 = 
1: ?m.15340
1 := 
Goals accomplished! πŸ™
s: β„•

h: s β‰  0

gcdA s 0 = 1
s: β„•

h: s β‰  0

(xgcdAux s 1 0 0 0 1).snd.fst = 1
s: β„•

h: s β‰  0

gcdA s 0 = 1
s: β„•

h: succ s β‰  0

intro
(xgcdAux (succ s) 1 0 0 0 1).snd.fst = 1
s: β„•

h: s β‰  0

gcdA s 0 = 1
s: β„•

h: succ s β‰  0

intro
(xgcdAux (succ s) 1 0 0 0 1).snd.fst = 1
s: β„•

h: succ s β‰  0

intro
(xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.fst = 1
s: β„•

h: succ s β‰  0

intro
(xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.fst = 1
s: β„•

h: s β‰  0

gcdA s 0 = 1
Goals accomplished! πŸ™

#align nat.gcd_a_zero_right 
Nat.gcdA_zero_right: βˆ€ {s : β„•}, s β‰  0 β†’ gcdA s 0 = 1
Nat.gcdA_zero_right

@[simp]
theorem 
gcdB_zero_right: βˆ€ {s : β„•}, s β‰  0 β†’ gcdB s 0 = 0
gcdB_zero_right {
s: β„•
s : 
β„•: Type
β„•} (
h: s β‰  0
h : 
s: β„•
s β‰  
0: ?m.15493
0) : 
gcdB: β„• β†’ β„• β†’ β„€
gcdB 
s: β„•
s 
0: ?m.15507
0 = 
0: ?m.15510
0 := 
Goals accomplished! πŸ™
s: β„•

h: s β‰  0

gcdB s 0 = 0
s: β„•

h: s β‰  0

(xgcdAux s 1 0 0 0 1).snd.snd = 0
s: β„•

h: s β‰  0

gcdB s 0 = 0
s: β„•

h: succ s β‰  0

intro
(xgcdAux (succ s) 1 0 0 0 1).snd.snd = 0
s: β„•

h: s β‰  0

gcdB s 0 = 0
s: β„•

h: succ s β‰  0

intro
(xgcdAux (succ s) 1 0 0 0 1).snd.snd = 0
s: β„•

h: succ s β‰  0

intro
(xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.snd = 0
s: β„•

h: succ s β‰  0

intro
(xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.snd = 0
s: β„•

h: s β‰  0

gcdB s 0 = 0
Goals accomplished! πŸ™

#align nat.gcd_b_zero_right 
Nat.gcdB_zero_right: βˆ€ {s : β„•}, s β‰  0 β†’ gcdB s 0 = 0
Nat.gcdB_zero_right

@[simp]
theorem 
xgcd_aux_fst: βˆ€ (x y : β„•) (s t s' t' : β„€), (xgcdAux x s t y s' t').fst = gcd x y
xgcd_aux_fst (
x: β„•
x 
y: ?m.15661
y) : βˆ€ 
s: ?m.15665
s 
t: ?m.15668
t 
s': ?m.15671
s' 
t': ?m.15674
t', (
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux 
x: ?m.15658
x 
s: ?m.15665
s 
t: ?m.15668
t 
y: ?m.15661
y 
s': ?m.15671
s' 
t': ?m.15674
t').
1: {Ξ± : Type ?u.15679} β†’ {Ξ² : Type ?u.15678} β†’ Ξ± Γ— Ξ² β†’ Ξ±
1 = 
gcd: β„• β†’ β„• β†’ β„•
gcd 
x: ?m.15658
x 
y: ?m.15661
y :=
  
gcd.induction: βˆ€ {P : β„• β†’ β„• β†’ Prop} (m n : β„•), (βˆ€ (n : β„•), P 0 n) β†’ (βˆ€ (m n : β„•), 0 < m β†’ P (n % m) m β†’ P m n) β†’ P m n
gcd.induction 
x: β„•
x 
y: β„•
y (
Goals accomplished! πŸ™
x, y: β„•

βˆ€ (n : β„•) (s t s' t' : β„€), (xgcdAux 0 s t n s' t').fst = gcd 0 n
Goals accomplished! πŸ™
) fun 
x: ?m.15723
x 
y: ?m.15726
y 
h: ?m.15729
h 
IH: ?m.15732
IH 
s: ?m.15739
s 
t: ?m.15742
t 
s': ?m.15745
s' 
t': ?m.15748
t' => 
Goals accomplished! πŸ™
x✝, y✝, x, y: β„•

h: 0 < x

IH: βˆ€ (s t s' t' : β„€), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x

s, t, s', t': β„€

(xgcdAux x s t y s' t').fst = gcd x y
x✝, y✝, x, y: β„•

h: 0 < x

IH: βˆ€ (s t s' t' : β„€), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x

s, t, s', t': β„€

gcd (y % x) x = gcd x y
x✝, y✝, x, y: β„•

h: 0 < x

IH: βˆ€ (s t s' t' : β„€), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x

s, t, s', t': β„€

(xgcdAux x s t y s' t').fst = gcd x y
x✝, y✝, x, y: β„•

h: 0 < x

IH: βˆ€ (s t s' t' : β„€), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x

s, t, s', t': β„€

gcd (y % x) x = gcd x y
x✝, y✝, x, y: β„•

h: 0 < x

IH: βˆ€ (s t s' t' : β„€), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x

s, t, s', t': β„€

gcd x y = gcd x y
Goals accomplished! πŸ™

#align nat.xgcd_aux_fst 
Nat.xgcd_aux_fst: βˆ€ (x y : β„•) (s t s' t' : β„€), (xgcdAux x s t y s' t').fst = gcd x y
Nat.xgcd_aux_fst

theorem 
xgcd_aux_val: βˆ€ (x y : β„•), xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
xgcd_aux_val (
x: ?m.18011
x 
y: β„•
y) : 
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux 
x: ?m.18011
x 
1: ?m.18019
1 
0: ?m.18030
0 
y: ?m.18014
y 
0: ?m.18037
0 
1: ?m.18040
1 = (
gcd: β„• β†’ β„• β†’ β„•
gcd 
x: ?m.18011
x 
y: ?m.18014
y, 
xgcd: β„• β†’ β„• β†’ β„€ Γ— β„€
xgcd 
x: ?m.18011
x 
y: ?m.18014
y) := 
Goals accomplished! πŸ™
x, y: β„•

xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
x, y: β„•

xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
x, y: β„•

xgcdAux x 1 0 y 0 1 = (gcd x y, (xgcdAux x 1 0 y 0 1).snd)
x, y: β„•

xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
x, y: β„•

xgcdAux x 1 0 y 0 1 = ((xgcdAux x 1 0 y 0 1).fst, (xgcdAux x 1 0 y 0 1).snd)
Goals accomplished! πŸ™

#align nat.xgcd_aux_val 
Nat.xgcd_aux_val: βˆ€ (x y : β„•), xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
Nat.xgcd_aux_val

theorem 
xgcd_val: βˆ€ (x y : β„•), xgcd x y = (gcdA x y, gcdB x y)
xgcd_val (
x: ?m.18087
x 
y: ?m.18090
y) : 
xgcd: β„• β†’ β„• β†’ β„€ Γ— β„€
xgcd 
x: ?m.18087
x 
y: ?m.18090
y = (
gcdA: β„• β†’ β„• β†’ β„€
gcdA 
x: ?m.18087
x 
y: ?m.18090
y, 
gcdB: β„• β†’ β„• β†’ β„€
gcdB 
x: ?m.18087
x 
y: ?m.18090
y) := 
Goals accomplished! πŸ™
x, y: β„•

xgcd x y = (gcdA x y, gcdB x y)
x, y: β„•

xgcd x y = ((xgcd x y).fst, (xgcd x y).snd)
x, y: β„•

xgcd x y = ((xgcd x y).fst, (xgcd x y).snd)
x, y: β„•

xgcd x y = (gcdA x y, gcdB x y)
x, y: β„•

fst✝, snd✝: β„€

mk
(fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
x, y: β„•

fst✝, snd✝: β„€

mk
(fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
x, y: β„•

xgcd x y = (gcdA x y, gcdB x y)
Goals accomplished! πŸ™

#align nat.xgcd_val 
Nat.xgcd_val: βˆ€ (x y : β„•), xgcd x y = (gcdA x y, gcdB x y)
Nat.xgcd_val

section

variable (
x: β„•
x 
y: β„•
y : 
β„•: Type
β„•)

private def 
P: β„• β†’ β„• β†’ β„• Γ— β„€ Γ— β„€ β†’ Prop
P : 
β„•: Type
β„• Γ— 
β„€: Type
β„€ Γ— 
β„€: Type
β„€ β†’ 
Prop: Type
Prop
  | (
r: β„•
r, 
s: β„€
s, 
t: β„€
t) => (
r: β„•
r : 
β„€: Type
β„€) = 
x: β„•
x * 
s: β„€
s + 
y: β„•
y * 
t: β„€
t

theorem 
xgcd_aux_P: βˆ€ {r r' : β„•} {s t s' t' : β„€}, Nat.P x y (r, s, t) β†’ Nat.P x y (r', s', t') β†’ Nat.P x y (xgcdAux r s t r' s' t')
xgcd_aux_P {
r: β„•
r 
r': β„•
r'} :
    βˆ€ {
s: ?m.18642
s 
t: ?m.18645
t 
s': ?m.18648
s' 
t': ?m.18651
t'}, 
P: β„• β†’ β„• β†’ β„• Γ— β„€ Γ— β„€ β†’ Prop
P 
x: β„•
x 
y: β„•
y (
r: ?m.18635
r, 
s: ?m.18642
s, 
t: ?m.18645
t) β†’ 
P: β„• β†’ β„• β†’ β„• Γ— β„€ Γ— β„€ β†’ Prop
P 
x: β„•
x 
y: β„•
y (
r': ?m.18638
r', 
s': ?m.18648
s', 
t': ?m.18651
t') β†’ 
P: β„• β†’ β„• β†’ β„• Γ— β„€ Γ— β„€ β†’ Prop
P 
x: β„•
x 
y: β„•
y (
xgcdAux: β„• β†’ β„€ β†’ β„€ β†’ β„• β†’ β„€ β†’ β„€ β†’ β„• Γ— β„€ Γ— β„€
xgcdAux 
r: ?m.18635
r 
s: ?m.18642
s 
t: ?m.18645
t 
r': ?m.18638
r' 
s': ?m.18648
s' 
t': ?m.18651
t') := 
Goals accomplished! πŸ™
x, y, r, r': β„•

βˆ€ {s t s' t' : β„€}, Nat.P x y (r, s, t) β†’ Nat.P x y (r', s', t') β†’ Nat.P x y (xgcdAux r s t r' s' t')
x, y, r, r': β„•

βˆ€ {s t s' t' : β„€}, Nat.P x y (r, s, t) β†’ Nat.P x y (r', s', t') β†’ Nat.P x y (xgcdAux r s t r' s' t')
x, y, n✝: β„•

H0
βˆ€ {s t s' t' : β„€}, Nat.P x y (0, s, t) β†’ Nat.P x y (n✝, s', t') β†’ Nat.P x y (xgcdAux 0 s t n✝ s' t')
Goals accomplished! πŸ™
x, y, r, r': β„•

βˆ€ {s t s' t' : β„€}, Nat.P x y (r, s, t) β†’ Nat.P x y (r', s', t') β†’ Nat.P x y (xgcdAux r s t r' s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

H1
βˆ€ {s t s' t' : β„€}, Nat.P x y (a, s, t) β†’ Nat.P x y (b, s', t') β†’ Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

s, t, s', t': β„€

p: Nat.P x y (a, s, t)

p': Nat.P x y (b, s', t')

H1
Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

H1
βˆ€ {s t s' t' : β„€}, Nat.P x y (a, s, t) β†’ Nat.P x y (b, s', t') β†’ Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

s, t, s', t': β„€

p: Nat.P x y (a, s, t)

p': Nat.P x y (b, s', t')

H1
Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

s, t, s', t': β„€

p: Nat.P x y (a, s, t)

p': Nat.P x y (b, s', t')

H1
Nat.P x y (xgcdAux (b % a) (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

s, t, s', t': β„€

p: Nat.P x y (a, s, t)

p': Nat.P x y (b, s', t')

H1
Nat.P x y (xgcdAux (b % a) (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

s, t, s', t': β„€

p: Nat.P x y (a, s, t)

p': Nat.P x y (b, s', t')

H1
Nat.P x y (xgcdAux (b % a) (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

H1
βˆ€ {s t s' t' : β„€}, Nat.P x y (a, s, t) β†’ Nat.P x y (b, s', t') β†’ Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

s, t, s', t': β„€

p: Nat.P x y (a, s, t)

p': Nat.P x y (b, s', t')

H1
Nat.P x y (b % a, s' - ↑b / ↑a * s, t' - ↑b / ↑a * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

s, t, s', t': β„€

p: Nat.P x y (a, s, t)

p': Nat.P x y (b, s', t')

H1
Nat.P x y (b % a, s' - ↑b / ↑a * s, t' - ↑b / ↑a * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

H1
βˆ€ {s t s' t' : β„€}, Nat.P x y (a, s, t) β†’ Nat.P x y (b, s', t') β†’ Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

H1
↑b % ↑a = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

H1
βˆ€ {s t s' t' : β„€}, Nat.P x y (a, s, t) β†’ Nat.P x y (b, s', t') β†’ Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

H1
↑b % ↑a = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

H1
↑b - ↑a * (↑b / ↑a) = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

H1
↑b - ↑a * (↑b / ↑a) = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

H1
↑b - ↑a * (↑b / ↑a) = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

H1
βˆ€ {s t s' t' : β„€}, Nat.P x y (a, s, t) β†’ Nat.P x y (b, s', t') β†’ Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€}, Nat.P x y (b % a, s, t) β†’ Nat.P x y (a, s', t') β†’ Nat.P x y (xgcdAux (b % a) s t a s' t')

H1
βˆ€ {s t s' t' : β„€}, Nat.P x y (a, s, t) β†’ Nat.P x y (b, s', t') β†’ Nat.P x y (xgcdAux a s t b s' t')
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - (↑x * s + ↑y * t) * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s + ↑y * t) * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s + ↑y * t) * k = ↑x * s' - ↑x * (k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s + ↑y * t) * k = ↑x * s' + ↑y * (t' - k * t) - ↑x * (k * s)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s + ↑y * t) * k = ↑x * s' + (↑y * t' - ↑y * (k * t)) - ↑x * (k * s)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (k * t)) - ↑x * (k * s)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (t * k)) - ↑x * (k * s)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (t * k)) - ↑x * (s * k)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * t * k) - ↑x * (s * k)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * t * k) - ↑x * s * k
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑y * t * k + ↑x * s * k) = ↑x * s' + (↑y * t' - ↑y * t * k) - ↑x * s * k
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑y * t * k + ↑x * s * k) = ↑x * s' + ↑y * t' - ↑y * t * k - ↑x * s * k
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
x, y, a, b: β„•

h: 0 < a

IH: βˆ€ {s t s' t' : β„€},
  ↑b % ↑a = ↑x * s + ↑y * t β†’
    ↑a = ↑x * s' + ↑y * t' β†’
      ↑(xgcdAux (b % a) s t a s' t').fst =         ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd

s, t, s', t': β„€

p: ↑a = ↑x * s + ↑y * t

p': ↑b = ↑x * s' + ↑y * t'

k: β„€

H1
↑x * s' + ↑y * t' - (↑y * t * k + ↑x * s * k) = ↑x * s' + ↑y * t' - (↑y * t * k + ↑x * s * k)
Goals accomplished! πŸ™

set_option linter.uppercaseLean3 false in
#align nat.xgcd_aux_P 
Nat.xgcd_aux_P: βˆ€ (x y : β„•) {r r' : β„•} {s t s' t' : β„€},
  Nat.P x y (r, s, t) β†’ Nat.P x y (r', s', t') β†’ Nat.P x y (xgcdAux r s t r' s' t')
Nat.xgcd_aux_P

/-- **BΓ©zout's lemma**: given `x y : β„•`, `gcd x y = x * a + y * b`, where `a = gcd_a x y` and
`b = gcd_b x y` are computed by the extended Euclidean algorithm.
-/
theorem 
gcd_eq_gcd_ab: ↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
gcd_eq_gcd_ab : (
gcd: β„• β†’ β„• β†’ β„•
gcd 
x: β„•
x 
y: β„•
y : 
β„€: Type
β„€) = 
x: β„•
x * 
gcdA: β„• β†’ β„• β†’ β„€
gcdA 
x: β„•
x 
y: β„•
y + 
y: β„•
y * 
gcdB: β„• β†’ β„• β†’ β„€
gcdB 
x: β„•
x 
y: β„•
y := 
Goals accomplished! πŸ™
x, y: β„•

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x, y: β„•

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
Goals accomplished! πŸ™
x, y: β„•

Nat.P x y (x, 1, 0)
Goals accomplished! πŸ™
x, y: β„•

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
Goals accomplished! πŸ™
x, y: β„•

Nat.P x y (y, 0, 1)
Goals accomplished! πŸ™
x, y: β„•

this: Nat.P x y (xgcdAux x 1 0 y 0 1)

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x, y: β„•

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x, y: β„•

this: Nat.P x y (xgcdAux x 1 0 y 0 1)

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x, y: β„•

this: Nat.P x y (gcd x y, xgcd x y)

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x, y: β„•

this: Nat.P x y (xgcdAux x 1 0 y 0 1)

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x, y: β„•

this: Nat.P x y (gcd x y, gcdA x y, gcdB x y)

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x, y: β„•

this: Nat.P x y (gcd x y, gcdA x y, gcdB x y)

↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
Goals accomplished! πŸ™

#align nat.gcd_eq_gcd_ab 
Nat.gcd_eq_gcd_ab: βˆ€ (x y : β„•), ↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
Nat.gcd_eq_gcd_ab

end

theorem 
exists_mul_emod_eq_gcd: βˆ€ {k n : β„•}, gcd n k < k β†’ βˆƒ m, n * m % k = gcd n k
exists_mul_emod_eq_gcd {
k: β„•
k 
n: β„•
n : 
β„•: Type
β„•} (
hk: gcd n k < k
hk : 
gcd: β„• β†’ β„• β†’ β„•
gcd 
n: β„•
n 
k: β„•
k < 
k: β„•
k) : βˆƒ 
m: ?m.23157
m, 
n: β„•
n * 
m: ?m.23157
m % 
k: β„•
k = 
gcd: β„• β†’ β„• β†’ β„•
gcd 
n: β„•
n 
k: β„•
k := 
Goals accomplished! πŸ™
k, n: β„•

hk: gcd n k < k

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: (fun m => Int.toNat (m % ↑k)) ↑(gcd n k) = (fun m => Int.toNat (m % ↑k)) (↑n * gcdA n k + ↑k * gcdB n k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: Int.toNat (↑(gcd n k) % ↑k) = Int.toNat (↑n * gcdA n k % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: Int.toNat ↑(gcd n k % k) = Int.toNat (↑n * gcdA n k % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k % k = Int.toNat (↑n * gcdA n k % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

βˆƒ m, n * m % k = gcd n k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑(n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑(n * Int.toNat (gcdA n k % ↑k)) % ↑k = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑n * ↑(Int.toNat (gcdA n k % ↑k)) % ↑k = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑n * (gcdA n k % ↑k) % ↑k = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑n * (gcdA n k % ↑k) % ↑k = ↑(Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑n * (gcdA n k % ↑k) % ↑k = ↑n * gcdA n k % ↑k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑n % ↑k * (gcdA n k % ↑k % ↑k) % ↑k = ↑n * gcdA n k % ↑k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑n % ↑k * (gcdA n k % ↑k) % ↑k = ↑n * gcdA n k % ↑k
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k, n: β„•

hk: gcd n k < k

hk': ↑k β‰  0

key: gcd n k = Int.toNat (↑n * gcdA n k % ↑k)

↑n * gcdA n k % ↑k = ↑n * gcdA n k % ↑k
Goals accomplished! πŸ™

#align nat.exists_mul_mod_eq_gcd 
Nat.exists_mul_emod_eq_gcd: βˆ€ {k n : β„•}, gcd n k < k β†’ βˆƒ m, n * m % k = gcd n k
Nat.exists_mul_emod_eq_gcd

theorem 
exists_mul_emod_eq_one_of_coprime: βˆ€ {k n : β„•}, coprime n k β†’ 1 < k β†’ βˆƒ m, n * m % k = 1
exists_mul_emod_eq_one_of_coprime {
k: β„•
k 
n: β„•
n : 
β„•: Type
β„•} (
hkn: coprime n k
hkn : 
coprime: β„• β†’ β„• β†’ Prop
coprime 
n: β„•
n 
k: β„•
k) (
hk: 1 < k
hk : 
1: ?m.23861
1 < 
k: β„•
k) :
    βˆƒ 
m: ?m.23899
m, 
n: β„•
n * 
m: ?m.23899
m % 
k: β„•
k = 
1: ?m.23909
1 :=
  
Exists.recOn: βˆ€ {Ξ± : Sort ?u.24008} {p : Ξ± β†’ Prop} {motive : Exists p β†’ Prop} (t : Exists p),
  (βˆ€ (w : Ξ±) (h : p w), motive (_ : Exists p)) β†’ motive t
Exists.recOn (
exists_mul_emod_eq_gcd: βˆ€ {k n : β„•}, gcd n k < k β†’ βˆƒ m, n * m % k = gcd n k
exists_mul_emod_eq_gcd (
lt_of_le_of_lt: βˆ€ {Ξ± : Type ?u.24037} [inst : Preorder Ξ±] {a b c : Ξ±}, a ≀ b β†’ b < c β†’ a < c
lt_of_le_of_lt (
le_of_eq: βˆ€ {Ξ± : Type ?u.24114} [inst : Preorder Ξ±] {a b : Ξ±}, a = b β†’ a ≀ b
le_of_eq 
hkn: coprime n k
hkn) 
hk: 1 < k
hk)) fun 
m: ?m.24157
m 
hm: ?m.24160
hm ↦
    ⟨
m: ?m.24157
m, 
hm: ?m.24160
hm.
trans: βˆ€ {Ξ± : Sort ?u.24171} {a b c : Ξ±}, a = b β†’ b = c β†’ a = c
trans 
hkn: coprime n k
hkn⟩
#align nat.exists_mul_mod_eq_one_of_coprime 
Nat.exists_mul_emod_eq_one_of_coprime: βˆ€ {k n : β„•}, coprime n k β†’ 1 < k β†’ βˆƒ m, n * m % k = 1
Nat.exists_mul_emod_eq_one_of_coprime

end Nat

/-! ### Divisibility over β„€ -/


namespace Int

theorem 
gcd_def: βˆ€ (i j : β„€), gcd i j = Nat.gcd (natAbs i) (natAbs j)
gcd_def (
i: β„€
i 
j: β„€
j : 
β„€: Type
β„€) : 
gcd: β„€ β†’ β„€ β†’ β„•
gcd 
i: β„€
i 
j: β„€
j = 
Nat.gcd: β„• β†’ β„• β†’ β„•
Nat.gcd 
i: β„€
i.
natAbs: β„€ β†’ β„•
natAbs 
j: β„€
j.
natAbs: β„€ β†’ β„•
natAbs := 
rfl: βˆ€ {Ξ± : Sort ?u.24207} {a : Ξ±}, a = a
rfl

protected theorem 
coe_nat_gcd: βˆ€ (m n : β„•), gcd ↑m ↑n = Nat.gcd m n
coe_nat_gcd (
m: β„•
m 
n: β„•
n : 
β„•: Type
β„•) : 
Int.gcd: β„€ β†’ β„€ β†’ β„•
Int.gcd ↑
m: β„•
m ↑
n: β„•
n = 
Nat.gcd: β„• β†’ β„• β†’ β„•
Nat.gcd 
m: β„•
m 
n: β„•
n :=
  
rfl: βˆ€ {Ξ± : Sort ?u.24316} {a : Ξ±}, a = a
rfl
#align int.coe_nat_gcd 
Int.coe_nat_gcd: βˆ€ (m n : β„•), gcd ↑m ↑n = Nat.gcd m n
Int.coe_nat_gcd

/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
def 
gcdA: β„€ β†’ β„€ β†’ β„€
gcdA : 
β„€: Type
β„€ β†’ 
β„€: Type
β„€ β†’ 
β„€: Type
β„€
  | 
ofNat: β„• β†’ β„€
ofNat 
m: β„•
m, 
n: β„€
n => 
m: β„•
m.
gcdA: β„• β†’ β„• β†’ β„€
gcdA 
n: β„€
n.
natAbs: β„€ β†’ β„•
natAbs
  | -[
m: β„•
m+1], 
n: β„€
n => -
m: β„•
m.
succ: β„• β†’ β„•
succ.
gcdA: β„• β†’ β„• β†’ β„€
gcdA 
n: β„€
n.
natAbs: β„€ β†’ β„•
natAbs
#align int.gcd_a 
Int.gcdA: β„€ β†’ β„€ β†’ β„€
Int.gcdA

/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
def 
gcdB: β„€ β†’ β„€ β†’ β„€
gcdB : 
β„€: Type
β„€ β†’ 
β„€: Type
β„€ β†’ 
β„€: Type
β„€
  | 
m: β„€
m, 
ofNat: β„• β†’ β„€
ofNat 
n: β„•
n => 
m: β„€
m.
natAbs: β„€ β†’ β„•
natAbs.
gcdB: β„• β†’ β„• β†’ β„€
gcdB 
n: β„•
n
  | 
m: β„€
m, -[
n: β„•
n+1] => -
m: β„€
m.
natAbs: β„€ β†’ β„•
natAbs.
gcdB: β„• β†’ β„• β†’ β„€
gcdB 
n: β„•
n.
succ: β„• β†’ β„•
succ
#align int.gcd_b 
Int.gcdB: β„€ β†’ β„€ β†’ β„€
Int.gcdB

/-- **BΓ©zout's lemma** -/
theorem 
gcd_eq_gcd_ab: βˆ€ (x y : β„€), ↑(gcd x y) = x * gcdA x y + y * gcdB x y
gcd_eq_gcd_ab : βˆ€ 
x: β„€
x 
y: β„€
y : 
β„€: Type
β„€, (
gcd: β„€ β†’ β„€ β†’ β„•
gcd 
x: β„€
x 
y: β„€
y : 
β„€: Type
β„€) = 
x: β„€
x * 
gcdA: β„€ β†’ β„€ β†’ β„€
gcdA 
x: β„€
x 
y: β„€
y + 
y: β„€
y * 
gcdB: β„€ β†’ β„€ β†’ β„€
gcdB 
x: β„€
x 
y: β„€
y
  | (m : β„•), (n : β„•) => 
Nat.gcd_eq_gcd_ab: βˆ€ (x y : β„•), ↑(Nat.gcd x y) = ↑x * Nat.gcdA x y + ↑y * Nat.gcdB x y
Nat.gcd_eq_gcd_ab 
_: β„•
_ 
_: β„•
_
  | (m : β„•), -[
n: β„•
n+1] =>
    show (
_: β„€
_ : 
β„€: Type
β„€) = 
_: ?m.25255
_ + -(
n: β„•
n + 
1: ?m.25265
1) * -
_: ?m.25277
_ by 
m, n: β„•

↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + -(↑n + 1) * -Nat.gcdB (natAbs ↑m) (Nat.succ n)
m, n: β„•

↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + (↑n + 1) * Nat.gcdB (natAbs ↑m) (Nat.succ n)
m, n: β„•

↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + (↑n + 1) * Nat.gcdB (natAbs ↑m) (Nat.succ n)
m, n: β„•

↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + (↑n + 1) * Nat.gcdB (natAbs ↑m) (Nat.succ n)
m, n: β„•

↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + -(↑n + 1) * -Nat.gcdB (natAbs ↑m) (Nat.succ n)
Goals accomplished! πŸ™

  | -[
m: β„•
m+1], (n : β„•) =>
    show (
_: β„€
_ : 
β„€: Type
β„€) = -(
m: β„•
m + 
1: ?m.25595
1) * -
_: ?m.25607
_ + 
_: ?m.25610
_ by 
m, n: β„•

↑(gcd -[m+1] ↑n) = -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
m, n: β„•

↑(gcd -[m+1] ↑n) = (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
m, n: β„•

↑(gcd -[m+1] ↑n) = (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
m, n: β„•

↑(gcd -[m+1] ↑n) = (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
m, n: β„•

↑(gcd -[m+1] ↑n) = -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
Goals accomplished! πŸ™

  | -[
m: β„•
m+1], -[
n: β„•
n+1] =>
    show (
_: β„€
_ : 
β„€: Type
β„€) = -(
m: β„•
m + 
1: ?m.25849
1) * -
_: ?m.25861
_ + -(
n: β„•
n + 
1: ?m.25871
1) * -
_: ?m.25883
_ by
      
m, n: β„•

↑(gcd -[m+1] -[n+1]) =   -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + -(↑n + 1) * -Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
m, n: β„•

↑(gcd -[m+1] -[n+1]) =   (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + -(↑n + 1) * -Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
m, n: β„•

↑(gcd -[m+1] -[n+1]) =   -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + -(↑n + 1) * -Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
m, n: β„•

↑(gcd -[m+1] -[n+1]) =   (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + (↑n + 1) * Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
m, n: β„•

↑(gcd -[m+1] -[n+1]) =   (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + (↑n + 1) * Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
m, n: β„•

↑(gcd -[m+1] -[n+1]) =   -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + -(↑n + 1) * -Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
Goals accomplished! πŸ™

#align int.gcd_eq_gcd_ab 
Int.gcd_eq_gcd_ab: βˆ€ (x y : β„€), ↑(gcd x y) = x * gcdA x y + y * gcdB x y
Int.gcd_eq_gcd_ab

theorem 
natAbs_ediv: βˆ€ (a b : β„€), b ∣ a β†’ natAbs (a / b) = natAbs a / natAbs b
natAbs_ediv (
a: β„€
a 
b: β„€
b : 
β„€: Type
β„€) (
H: b ∣ a
H : 
b: β„€
b ∣ 
a: β„€
a) : 
natAbs: β„€ β†’ β„•
natAbs (
a: β„€
a / 
b: β„€
b) = 
natAbs: β„€ β†’ β„•
natAbs 
a: β„€
a / 
natAbs: β„€ β†’ β„•
natAbs 
b: β„€
b := 
Goals accomplished! πŸ™
a, b: β„€

H: b ∣ a

natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b = 0

inl
natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b = 0

inl
natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b = 0

inl
natAbs (a / 0) = natAbs a / natAbs 0
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b = 0

inl
natAbs (a / 0) = natAbs a / natAbs 0
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

natAbs (a / b) = natAbs a / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
Goals accomplished! πŸ™
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) = natAbs (a / b) * 1
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) = natAbs (a / b) * 1
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) = natAbs (a / b)
Goals accomplished! πŸ™
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
Goals accomplished! πŸ™
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) * 1 = natAbs (a / b) * (natAbs b / natAbs b)
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) * 1 = natAbs (a / b) * (natAbs b / natAbs b)
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) * 1 = natAbs (a / b) * 1
Goals accomplished! πŸ™
a, b: β„€

H: b ∣ a

h: natAbs b > 0

inr
natAbs (a / b) = natAbs a / natAbs b
Goals accomplished! πŸ™
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) * (natAbs b / natAbs b) = natAbs (a / b) * natAbs b / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) * (natAbs b / natAbs b) = natAbs (a / b) * natAbs b / natAbs b
a, b: β„€

H: b ∣ a

h: natAbs b > 0

natAbs (a / b) * (natAbs b / natAbs b) = natAbs (a / b) * (natAbs b / natAbs b)
Goals accomplished! πŸ™
a, b: