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) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Mario Carneiro
-/
import Std.Data.Int.Lemmas

/-!
# Lemmas about integer division
-/


open Nat

namespace Int

/-! ### `/`  -/

theorem 
ofNat_div: โˆ€ (m n : Nat), โ†‘(m / n) = div โ†‘m โ†‘n
ofNat_div
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) : โ†‘(
m: Nat
m
/
n: Nat
n
) =
div: Int โ†’ Int โ†’ Int
div
โ†‘
m: Nat
m
โ†‘
n: Nat
n
:=
rfl: โˆ€ {ฮฑ : Sort ?u.133} {a : ฮฑ}, a = a
rfl
theorem
ofNat_fdiv: โˆ€ (m n : Nat), โ†‘(m / n) = fdiv โ†‘m โ†‘n
ofNat_fdiv
: โˆ€
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
, โ†‘(
m: Nat
m
/
n: Nat
n
) =
fdiv: Int โ†’ Int โ†’ Int
fdiv
โ†‘
m: Nat
m
โ†‘
n: Nat
n
|
0: Nat
0
, _ =>

Goals accomplished! ๐Ÿ™
xโœ: Nat


โ†‘(0 / xโœ) = fdiv โ†‘0 โ†‘xโœ

Goals accomplished! ๐Ÿ™
|
succ: Nat โ†’ Nat
succ
_, _ =>
rfl: โˆ€ {ฮฑ : Sort ?u.330} {a : ฮฑ}, a = a
rfl
@[simp, norm_cast] theorem
ofNat_ediv: โˆ€ (m n : Nat), โ†‘(m / n) = โ†‘m / โ†‘n
ofNat_ediv
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) : (โ†‘(
m: Nat
m
/
n: Nat
n
) :
Int: Type
Int
) = โ†‘
m: Nat
m
/ โ†‘
n: Nat
n
:=
rfl: โˆ€ {ฮฑ : Sort ?u.673} {a : ฮฑ}, a = a
rfl
theorem
negSucc_ediv: โˆ€ (m : Nat) {b : Int}, 0 < b โ†’ -[m+1] / b = -(div (โ†‘m) b + 1)
negSucc_ediv
(
m: Nat
m
:
Nat: Type
Nat
) {
b: Int
b
:
Int: Type
Int
} (
H: 0 < b
H
:
0: ?m.795
0
<
b: Int
b
) : -[
m: Nat
m
+1] /
b: Int
b
= -(
div: Int โ†’ Int โ†’ Int
div
m: Nat
m
b: Int
b
+
1: ?m.865
1
) := match
b: Int
b
,
eq_succ_of_zero_lt: โˆ€ {a : Int}, 0 < a โ†’ โˆƒ n, a = โ†‘(succ n)
eq_succ_of_zero_lt
H: 0 < b
H
with | _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.964} {a : ฮฑ}, a = a
rfl
โŸฉ =>
rfl: โˆ€ {ฮฑ : Sort ?u.1024} {a : ฮฑ}, a = a
rfl
@[simp] protected theorem
zero_div: โˆ€ (b : Int), div 0 b = 0
zero_div
: โˆ€
b: Int
b
:
Int: Type
Int
,
div: Int โ†’ Int โ†’ Int
div
0: ?m.1313
0
b: Int
b
=
0: ?m.1322
0
|
ofNat: Nat โ†’ Int
ofNat
_ => show
ofNat: Nat โ†’ Int
ofNat
_: Nat
_
=
_: ?m.1355
_
by

Goals accomplished! ๐Ÿ™
| -[_+1] => show -
ofNat: Nat โ†’ Int
ofNat
_: Nat
_
=
_: ?m.1405
_
by

Goals accomplished! ๐Ÿ™
@[local simp] theorem
zero_ediv: โˆ€ (b : Int), 0 / b = 0
zero_ediv
: โˆ€
b: Int
b
:
Int: Type
Int
,
0: ?m.1740
0
/
b: Int
b
=
0: ?m.1752
0
|
ofNat: Nat โ†’ Int
ofNat
_ => show
ofNat: Nat โ†’ Int
ofNat
_: Nat
_
=
_: ?m.1821
_
by

Goals accomplished! ๐Ÿ™
| -[_+1] => show -
ofNat: Nat โ†’ Int
ofNat
_: Nat
_
=
_: ?m.1876
_
by

Goals accomplished! ๐Ÿ™
@[simp] theorem
zero_fdiv: โˆ€ (b : Int), fdiv 0 b = 0
zero_fdiv
(
b: Int
b
:
Int: Type
Int
) :
fdiv: Int โ†’ Int โ†’ Int
fdiv
0: ?m.2710
0
b: Int
b
=
0: ?m.2719
0
:=

Goals accomplished! ๐Ÿ™
b: Int


fdiv 0 b = 0
aโœ: Nat


ofNat
fdiv 0 (ofNat aโœ) = 0
aโœ: Nat


negSucc
fdiv 0 -[aโœ+1] = 0
b: Int


fdiv 0 b = 0
aโœ: Nat


ofNat
fdiv 0 (ofNat aโœ) = 0
aโœ: Nat


negSucc
fdiv 0 -[aโœ+1] = 0
b: Int


fdiv 0 b = 0

Goals accomplished! ๐Ÿ™
@[simp] protected theorem
div_zero: โˆ€ (a : Int), div a 0 = 0
div_zero
: โˆ€
a: Int
a
:
Int: Type
Int
,
div: Int โ†’ Int โ†’ Int
div
a: Int
a
0: ?m.2838
0
=
0: ?m.2847
0
|
ofNat: Nat โ†’ Int
ofNat
_ => show
ofNat: Nat โ†’ Int
ofNat
_: Nat
_
=
_: ?m.2880
_
by

Goals accomplished! ๐Ÿ™
| -[_+1] =>
rfl: โˆ€ {ฮฑ : Sort ?u.2925} {a : ฮฑ}, a = a
rfl
-- Will be generalized to Euclidean domains. @[local simp] protected theorem
ediv_zero: โˆ€ (a : Int), a / 0 = 0
ediv_zero
: โˆ€
a: Int
a
:
Int: Type
Int
,
a: Int
a
/
0: ?m.3111
0
=
0: ?m.3123
0
|
ofNat: Nat โ†’ Int
ofNat
_ => show
ofNat: Nat โ†’ Int
ofNat
_: Nat
_
=
_: ?m.3192
_
by

Goals accomplished! ๐Ÿ™
| -[_+1] =>
rfl: โˆ€ {ฮฑ : Sort ?u.3242} {a : ฮฑ}, a = a
rfl
@[simp] protected theorem
fdiv_zero: โˆ€ (a : Int), fdiv a 0 = 0
fdiv_zero
: โˆ€
a: Int
a
:
Int: Type
Int
,
fdiv: Int โ†’ Int โ†’ Int
fdiv
a: Int
a
0: ?m.3391
0
=
0: ?m.3400
0
|
0: Int
0
=>
rfl: โˆ€ {ฮฑ : Sort ?u.3423} {a : ฮฑ}, a = a
rfl
|
succ: Nat โ†’ Nat
succ
_ =>
rfl: โˆ€ {ฮฑ : Sort ?u.3496} {a : ฮฑ}, a = a
rfl
| -[_+1] =>
rfl: โˆ€ {ฮฑ : Sort ?u.3545} {a : ฮฑ}, a = a
rfl
theorem
fdiv_eq_ediv: โˆ€ (a : Int) {b : Int}, 0 โ‰ค b โ†’ fdiv a b = a / b
fdiv_eq_ediv
: โˆ€ (
a: Int
a
:
Int: Type
Int
) {
b: Int
b
:
Int: Type
Int
},
0: ?m.3675
0
โ‰ค
b: Int
b
โ†’
fdiv: Int โ†’ Int โ†’ Int
fdiv
a: Int
a
b: Int
b
=
a: Int
a
/
b: Int
b
|
0: Int
0
, _, _ | -[_+1],
0: Int
0
, _ =>

Goals accomplished! ๐Ÿ™
aโœ: Nat

xโœ: 0 โ‰ค 0


fdiv -[aโœ+1] 0 = -[aโœ+1] / 0

Goals accomplished! ๐Ÿ™
|
succ: Nat โ†’ Nat
succ
_,
ofNat: Nat โ†’ Int
ofNat
_, _ | -[_+1],
succ: Nat โ†’ Nat
succ
_, _ =>
rfl: โˆ€ {ฮฑ : Sort ?u.3951} {a : ฮฑ}, a = a
rfl
theorem
div_eq_ediv: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ div a b = a / b
div_eq_ediv
: โˆ€ {
a: Int
a
b: Int
b
:
Int: Type
Int
},
0: ?m.4634
0
โ‰ค
a: Int
a
โ†’
0: ?m.4662
0
โ‰ค
b: Int
b
โ†’
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
b: Int
b
=
a: Int
a
/
b: Int
b
|
0: Int
0
, _, _, _ | _,
0: Int
0
, _, _ =>

Goals accomplished! ๐Ÿ™
xโœยฒ: Int

xโœยน: 0 โ‰ค xโœยฒ

xโœ: 0 โ‰ค 0


div xโœยฒ 0 = xโœยฒ / 0

Goals accomplished! ๐Ÿ™
|
succ: Nat โ†’ Nat
succ
_,
succ: Nat โ†’ Nat
succ
_, _, _ =>
rfl: โˆ€ {ฮฑ : Sort ?u.4884} {a : ฮฑ}, a = a
rfl
theorem
fdiv_eq_div: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ fdiv a b = div a b
fdiv_eq_div
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
Ha: 0 โ‰ค a
Ha
:
0: ?m.6091
0
โ‰ค
a: Int
a
) (
Hb: 0 โ‰ค b
Hb
:
0: ?m.6119
0
โ‰ค
b: Int
b
) :
fdiv: Int โ†’ Int โ†’ Int
fdiv
a: Int
a
b: Int
b
=
div: Int โ†’ Int โ†’ Int
div
a: Int
a
b: Int
b
:=
div_eq_ediv: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ div a b = a / b
div_eq_ediv
Ha: 0 โ‰ค a
Ha
Hb: 0 โ‰ค b
Hb
โ–ธ
fdiv_eq_ediv: โˆ€ (a : Int) {b : Int}, 0 โ‰ค b โ†’ fdiv a b = a / b
fdiv_eq_ediv
_: Int
_
Hb: 0 โ‰ค b
Hb
@[simp] protected theorem
div_neg: โˆ€ (a b : Int), div a (-b) = -div a b
div_neg
: โˆ€
a: Int
a
b: Int
b
:
Int: Type
Int
,
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
(-
b: Int
b
) = -(
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
b: Int
b
) |
ofNat: Nat โ†’ Int
ofNat
m: Nat
m
,
0: Int
0
=> show
ofNat: Nat โ†’ Int
ofNat
(
m: Nat
m
/
0: ?m.6225
0
) = -โ†‘(
m: Nat
m
/
0: ?m.6280
0
) by
m: Nat


ofNat (m / 0) = -โ†‘(m / 0)
m: Nat


ofNat 0 = -โ†‘0
m: Nat


ofNat 0 = -โ†‘0
m: Nat


ofNat 0 = -โ†‘0
m: Nat


ofNat (m / 0) = -โ†‘(m / 0)

Goals accomplished! ๐Ÿ™
|
ofNat: Nat โ†’ Int
ofNat
m: Nat
m
, -[
n: Nat
n
+1] | -[
m: Nat
m
+1],
succ: Nat โ†’ Nat
succ
n: Nat
n
=> (
Int.neg_neg: โˆ€ (a : Int), - -a = a
Int.neg_neg
_: Int
_
).
symm: โˆ€ {ฮฑ : Sort ?u.6519} {a b : ฮฑ}, a = b โ†’ b = a
symm
|
ofNat: Nat โ†’ Int
ofNat
m: Nat
m
,
succ: Nat โ†’ Nat
succ
n: Nat
n
| -[
m: Nat
m
+1],
0: Int
0
| -[
m: Nat
m
+1], -[
n: Nat
n
+1] =>
rfl: โˆ€ {ฮฑ : Sort ?u.6731} {a : ฮฑ}, a = a
rfl
@[simp] protected theorem
ediv_neg: โˆ€ (a b : Int), a / -b = -(a / b)
ediv_neg
: โˆ€
a: Int
a
b: Int
b
:
Int: Type
Int
,
a: Int
a
/ (-
b: Int
b
) = -(
a: Int
a
/
b: Int
b
) |
ofNat: Nat โ†’ Int
ofNat
m: Nat
m
,
0: Int
0
=> show
ofNat: Nat โ†’ Int
ofNat
(
m: Nat
m
/
0: ?m.7134
0
) = -โ†‘(
m: Nat
m
/
0: ?m.7181
0
) by
m: Nat


ofNat (m / 0) = -โ†‘(m / 0)
m: Nat


ofNat 0 = -โ†‘0
m: Nat


ofNat 0 = -โ†‘0
m: Nat


ofNat 0 = -โ†‘0
m: Nat


ofNat (m / 0) = -โ†‘(m / 0)

Goals accomplished! ๐Ÿ™
|
ofNat: Nat โ†’ Int
ofNat
m: Nat
m
, -[
n: Nat
n
+1] => (
Int.neg_neg: โˆ€ (a : Int), - -a = a
Int.neg_neg
_: Int
_
).
symm: โˆ€ {ฮฑ : Sort ?u.7352} {a b : ฮฑ}, a = b โ†’ b = a
symm
|
ofNat: Nat โ†’ Int
ofNat
m: Nat
m
,
succ: Nat โ†’ Nat
succ
n: Nat
n
| -[
m: Nat
m
+1],
0: Int
0
| -[
m: Nat
m
+1],
succ: Nat โ†’ Nat
succ
n: Nat
n
| -[
m: Nat
m
+1], -[
n: Nat
n
+1] =>
rfl: โˆ€ {ฮฑ : Sort ?u.7707} {a : ฮฑ}, a = a
rfl
protected theorem
div_def: โˆ€ (a b : Int), a / b = ediv a b
div_def
(
a: Int
a
b: Int
b
:
Int: Type
Int
) :
a: Int
a
/
b: Int
b
=
Int.ediv: Int โ†’ Int โ†’ Int
Int.ediv
a: Int
a
b: Int
b
:=
rfl: โˆ€ {ฮฑ : Sort ?u.8063} {a : ฮฑ}, a = a
rfl
-- Lean 4 core provides an instance for `Div Int` using `Int.div`. -- Even though we provide a higher priority instance in `Std.Data.Int.Basic`, -- we provide a `simp` lemma here to unfold usages of that instance back to `Int.div`. @[simp] theorem
div_def': โˆ€ (a b : Int), a / b = div a b
div_def'
(
a: Int
a
b: Int
b
:
Int: Type
Int
) : @
HDiv.hDiv: {ฮฑ : Type ?u.8079} โ†’ {ฮฒ : Type ?u.8078} โ†’ {ฮณ : outParam (Type ?u.8077)} โ†’ [self : HDiv ฮฑ ฮฒ ฮณ] โ†’ ฮฑ โ†’ ฮฒ โ†’ ฮณ
HDiv.hDiv
Int: Type
Int
Int: Type
Int
Int: Type
Int
(@
instHDiv: {ฮฑ : Type ?u.8080} โ†’ [inst : Div ฮฑ] โ†’ HDiv ฮฑ ฮฑ ฮฑ
instHDiv
Int: Type
Int
Int.instDivInt: Div Int
Int.instDivInt
)
a: Int
a
b: Int
b
=
Int.div: Int โ†’ Int โ†’ Int
Int.div
a: Int
a
b: Int
b
:=
rfl: โˆ€ {ฮฑ : Sort ?u.8089} {a : ฮฑ}, a = a
rfl
@[simp] protected theorem
neg_div: โˆ€ (a b : Int), div (-a) b = -div a b
neg_div
: โˆ€
a: Int
a
b: Int
b
:
Int: Type
Int
, (-
a: Int
a
).
div: Int โ†’ Int โ†’ Int
div
b: Int
b
= -(
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
b: Int
b
) |
0: Int
0
,
n: Int
n
=>

Goals accomplished! ๐Ÿ™
n: Int


div (-0) n = -div 0 n

Goals accomplished! ๐Ÿ™
|
succ: Nat โ†’ Nat
succ
m: Nat
m
, (n:Nat) | -[
m: Nat
m
+1],
0: Int
0
| -[
m: Nat
m
+1], -[
n: Nat
n
+1] =>
rfl: โˆ€ {ฮฑ : Sort ?u.8303} {a : ฮฑ}, a = a
rfl
|
succ: Nat โ†’ Nat
succ
m: Nat
m
, -[
n: Nat
n
+1] | -[
m: Nat
m
+1],
succ: Nat โ†’ Nat
succ
n: Nat
n
=> (
Int.neg_neg: โˆ€ (a : Int), - -a = a
Int.neg_neg
_: Int
_
).
symm: โˆ€ {ฮฑ : Sort ?u.8546} {a b : ฮฑ}, a = b โ†’ b = a
symm
protected theorem
neg_div_neg: โˆ€ (a b : Int), div (-a) (-b) = div a b
neg_div_neg
(
a: Int
a
b: Int
b
:
Int: Type
Int
) : (-
a: Int
a
).
div: Int โ†’ Int โ†’ Int
div
(-
b: Int
b
) =
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
b: Int
b
:=

Goals accomplished! ๐Ÿ™
a, b: Int


div (-a) (-b) = div a b

Goals accomplished! ๐Ÿ™
protected theorem
div_nonneg: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ 0 โ‰ค div a b
div_nonneg
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
Ha: 0 โ‰ค a
Ha
:
0: ?m.9293
0
โ‰ค
a: Int
a
) (
Hb: 0 โ‰ค b
Hb
:
0: ?m.9321
0
โ‰ค
b: Int
b
) :
0: ?m.9341
0
โ‰ค
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
b: Int
b
:= match
a: Int
a
,
b: Int
b
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
Ha: 0 โ‰ค a
Ha
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
Hb: 0 โ‰ค b
Hb
with | _, _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.9393} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.9397} {a : ฮฑ}, a = a
rfl
โŸฉ =>
ofNat_zero_le: โˆ€ (n : Nat), 0 โ‰ค โ†‘n
ofNat_zero_le
_: Nat
_
theorem
fdiv_nonneg: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ 0 โ‰ค fdiv a b
fdiv_nonneg
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
Ha: 0 โ‰ค a
Ha
:
0: ?m.9915
0
โ‰ค
a: Int
a
) (
Hb: 0 โ‰ค b
Hb
:
0: ?m.9943
0
โ‰ค
b: Int
b
) :
0: ?m.9963
0
โ‰ค
a: Int
a
.
fdiv: Int โ†’ Int โ†’ Int
fdiv
b: Int
b
:= match
a: Int
a
,
b: Int
b
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
Ha: 0 โ‰ค a
Ha
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
Hb: 0 โ‰ค b
Hb
with | _, _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.10023} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.10027} {a : ฮฑ}, a = a
rfl
โŸฉ =>
ofNat_fdiv: โˆ€ (m n : Nat), โ†‘(m / n) = fdiv โ†‘m โ†‘n
ofNat_fdiv
.. โ–ธ
ofNat_zero_le: โˆ€ (n : Nat), 0 โ‰ค โ†‘n
ofNat_zero_le
_: Nat
_
theorem
ediv_nonneg: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ 0 โ‰ค a / b
ediv_nonneg
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
Ha: 0 โ‰ค a
Ha
:
0: ?m.10516
0
โ‰ค
a: Int
a
) (
Hb: 0 โ‰ค b
Hb
:
0: ?m.10544
0
โ‰ค
b: Int
b
) :
0: ?m.10564
0
โ‰ค
a: Int
a
/
b: Int
b
:= match
a: Int
a
,
b: Int
b
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
Ha: 0 โ‰ค a
Ha
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
Hb: 0 โ‰ค b
Hb
with | _, _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.10648} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.10652} {a : ฮฑ}, a = a
rfl
โŸฉ =>
ofNat_zero_le: โˆ€ (n : Nat), 0 โ‰ค โ†‘n
ofNat_zero_le
_: Nat
_
protected theorem
div_nonpos: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ b โ‰ค 0 โ†’ div a b โ‰ค 0
div_nonpos
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
Ha: 0 โ‰ค a
Ha
:
0: ?m.11155
0
โ‰ค
a: Int
a
) (
Hb: b โ‰ค 0
Hb
:
b: Int
b
โ‰ค
0: ?m.11183
0
) :
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
b: Int
b
โ‰ค
0: ?m.11202
0
:=
Int.nonpos_of_neg_nonneg: โˆ€ {a : Int}, 0 โ‰ค -a โ†’ a โ‰ค 0
Int.nonpos_of_neg_nonneg
<|
Int.div_neg: โˆ€ (a b : Int), div a (-b) = -div a b
Int.div_neg
.. โ–ธ
Int.div_nonneg: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ 0 โ‰ค div a b
Int.div_nonneg
Ha: 0 โ‰ค a
Ha
(
Int.neg_nonneg_of_nonpos: โˆ€ {a : Int}, a โ‰ค 0 โ†’ 0 โ‰ค -a
Int.neg_nonneg_of_nonpos
Hb: b โ‰ค 0
Hb
) theorem
fdiv_nonpos: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ b โ‰ค 0 โ†’ fdiv a b โ‰ค 0
fdiv_nonpos
: โˆ€ {
a: Int
a
b: Int
b
:
Int: Type
Int
},
0: ?m.11260
0
โ‰ค
a: Int
a
โ†’
b: Int
b
โ‰ค
0: ?m.11288
0
โ†’
a: Int
a
.
fdiv: Int โ†’ Int โ†’ Int
fdiv
b: Int
b
โ‰ค
0: ?m.11306
0
|
0: Int
0
,
0: Int
0
, _, _ |
0: Int
0
, -[_+1], _, _ |
succ: Nat โ†’ Nat
succ
_,
0: Int
0
, _, _ |
succ: Nat โ†’ Nat
succ
_, -[_+1], _, _ => โŸจ
_: Nat
_
โŸฉ theorem
ediv_nonpos: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ b โ‰ค 0 โ†’ a / b โ‰ค 0
ediv_nonpos
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
Ha: 0 โ‰ค a
Ha
:
0: ?m.13065
0
โ‰ค
a: Int
a
) (
Hb: b โ‰ค 0
Hb
:
b: Int
b
โ‰ค
0: ?m.13093
0
) :
a: Int
a
/
b: Int
b
โ‰ค
0: ?m.13113
0
:=
Int.nonpos_of_neg_nonneg: โˆ€ {a : Int}, 0 โ‰ค -a โ†’ a โ‰ค 0
Int.nonpos_of_neg_nonneg
<|
Int.ediv_neg: โˆ€ (a b : Int), a / -b = -(a / b)
Int.ediv_neg
.. โ–ธ
Int.ediv_nonneg: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ 0 โ‰ค b โ†’ 0 โ‰ค a / b
Int.ediv_nonneg
Ha: 0 โ‰ค a
Ha
(
Int.neg_nonneg_of_nonpos: โˆ€ {a : Int}, a โ‰ค 0 โ†’ 0 โ‰ค -a
Int.neg_nonneg_of_nonpos
Hb: b โ‰ค 0
Hb
) theorem
fdiv_neg': โˆ€ {a b : Int}, a < 0 โ†’ 0 < b โ†’ fdiv a b < 0
fdiv_neg'
: โˆ€ {
a: Int
a
b: Int
b
:
Int: Type
Int
},
a: Int
a
<
0: ?m.13206
0
โ†’
0: ?m.13231
0
<
b: Int
b
โ†’
a: Int
a
.
fdiv: Int โ†’ Int โ†’ Int
fdiv
b: Int
b
<
0: ?m.13252
0
| -[_+1],
succ: Nat โ†’ Nat
succ
_, _, _ =>
negSucc_lt_zero: โˆ€ (n : Nat), -[n+1] < 0
negSucc_lt_zero
_: Nat
_
theorem
ediv_neg': โˆ€ {a b : Int}, a < 0 โ†’ 0 < b โ†’ a / b < 0
ediv_neg'
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
Ha: a < 0
Ha
:
a: Int
a
<
0: ?m.14527
0
) (
Hb: 0 < b
Hb
:
0: ?m.14552
0
<
b: Int
b
) :
a: Int
a
/
b: Int
b
<
0: ?m.14575
0
:= match
a: Int
a
,
b: Int
b
,
eq_negSucc_of_lt_zero: โˆ€ {a : Int}, a < 0 โ†’ โˆƒ n, a = -[n+1]
eq_negSucc_of_lt_zero
Ha: a < 0
Ha
,
eq_succ_of_zero_lt: โˆ€ {a : Int}, 0 < a โ†’ โˆƒ n, a = โ†‘(succ n)
eq_succ_of_zero_lt
Hb: 0 < b
Hb
with | _, _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.14653} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.14657} {a : ฮฑ}, a = a
rfl
โŸฉ =>
negSucc_lt_zero: โˆ€ (n : Nat), -[n+1] < 0
negSucc_lt_zero
_: Nat
_
@[simp] protected theorem
div_one: โˆ€ (a : Int), div a 1 = a
div_one
: โˆ€
a: Int
a
:
Int: Type
Int
,
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
1: ?m.15180
1
=
a: Int
a
| (n:Nat) =>
congrArg: โˆ€ {ฮฑ : Sort ?u.15243} {ฮฒ : Sort ?u.15242} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
ofNat: Nat โ†’ Int
ofNat
(
Nat.div_one: โˆ€ (n : Nat), n / 1 = n
Nat.div_one
_: Nat
_
) | -[
n: Nat
n
+1] =>

Goals accomplished! ๐Ÿ™

Goals accomplished! ๐Ÿ™
@[simp] theorem
fdiv_one: โˆ€ (a : Int), fdiv a 1 = a
fdiv_one
: โˆ€
a: Int
a
:
Int: Type
Int
,
a: Int
a
.
fdiv: Int โ†’ Int โ†’ Int
fdiv
1: ?m.15511
1
=
a: Int
a
|
0: Int
0
=>
rfl: โˆ€ {ฮฑ : Sort ?u.15533} {a : ฮฑ}, a = a
rfl
|
succ: Nat โ†’ Nat
succ
_ =>
congrArg: โˆ€ {ฮฑ : Sort ?u.15607} {ฮฒ : Sort ?u.15606} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
Nat.cast: {R : Type ?u.15612} โ†’ [inst : NatCast R] โ†’ Nat โ†’ R
Nat.cast
(
Nat.div_one: โˆ€ (n : Nat), n / 1 = n
Nat.div_one
_: Nat
_
) | -[_+1] =>
congrArg: โˆ€ {ฮฑ : Sort ?u.15663} {ฮฒ : Sort ?u.15662} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
negSucc: Nat โ†’ Int
negSucc
(
Nat.div_one: โˆ€ (n : Nat), n / 1 = n
Nat.div_one
_: Nat
_
) @[simp] theorem
ediv_one: โˆ€ (a : Int), a / 1 = a
ediv_one
: โˆ€
a: Int
a
:
Int: Type
Int
,
a: Int
a
/
1: ?m.15797
1
=
a: Int
a
| (_:Nat) =>
congrArg: โˆ€ {ฮฑ : Sort ?u.15900} {ฮฒ : Sort ?u.15899} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
Nat.cast: {R : Type ?u.15905} โ†’ [inst : NatCast R] โ†’ Nat โ†’ R
Nat.cast
(
Nat.div_one: โˆ€ (n : Nat), n / 1 = n
Nat.div_one
_: Nat
_
) | -[_+1] =>
congrArg: โˆ€ {ฮฑ : Sort ?u.15964} {ฮฒ : Sort ?u.15963} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
negSucc: Nat โ†’ Int
negSucc
(
Nat.div_one: โˆ€ (n : Nat), n / 1 = n
Nat.div_one
_: Nat
_
) theorem
div_eq_zero_of_lt: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ a < b โ†’ div a b = 0
div_eq_zero_of_lt
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
H1: 0 โ‰ค a
H1
:
0: ?m.16065
0
โ‰ค
a: Int
a
) (
H2: a < b
H2
:
a: Int
a
<
b: Int
b
) :
a: Int
a
.
div: Int โ†’ Int โ†’ Int
div
b: Int
b
=
0: ?m.16102
0
:= match
a: Int
a
,
b: Int
b
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
H1: 0 โ‰ค a
H1
,
eq_succ_of_zero_lt: โˆ€ {a : Int}, 0 < a โ†’ โˆƒ n, a = โ†‘(succ n)
eq_succ_of_zero_lt
(
Int.lt_of_le_of_lt: โˆ€ {a b c : Int}, a โ‰ค b โ†’ b < c โ†’ a < c
Int.lt_of_le_of_lt
H1: 0 โ‰ค a
H1
H2: a < b
H2
) with | _, _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.16151} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.16163} {a : ฮฑ}, a = a
rfl
โŸฉ =>
congrArg: โˆ€ {ฮฑ : Sort ?u.16261} {ฮฒ : Sort ?u.16260} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
Nat.cast: {R : Type ?u.16266} โ†’ [inst : NatCast R] โ†’ Nat โ†’ R
Nat.cast
<|
Nat.div_eq_of_lt: โˆ€ {a b : Nat}, a < b โ†’ a / b = 0
Nat.div_eq_of_lt
<|
ofNat_lt: โˆ€ {n m : Nat}, โ†‘n < โ†‘m โ†” n < m
ofNat_lt
.
1: โˆ€ {a b : Prop}, (a โ†” b) โ†’ a โ†’ b
1
H2: โ†‘wโœยน < โ†‘(succ wโœ)
H2
theorem
ediv_eq_zero_of_lt: โˆ€ {a b : Int}, 0 โ‰ค a โ†’ a < b โ†’ a / b = 0
ediv_eq_zero_of_lt
{
a: Int
a
b: Int
b
:
Int: Type
Int
} (
H1: 0 โ‰ค a
H1
:
0: ?m.16712
0
โ‰ค
a: Int
a
) (
H2: a < b
H2
:
a: Int
a
<
b: Int
b
) :
a: Int
a
/
b: Int
b
=
0: ?m.16750
0
:= match
a: Int
a
,
b: Int
b
,
eq_ofNat_of_zero_le: โˆ€ {a : Int}, 0 โ‰ค a โ†’ โˆƒ n, a = โ†‘n
eq_ofNat_of_zero_le
H1: 0 โ‰ค a
H1
,
eq_succ_of_zero_lt: โˆ€ {a : Int}, 0 < a โ†’ โˆƒ n, a = โ†‘(succ n)
eq_succ_of_zero_lt
(
Int.lt_of_le_of_lt: โˆ€ {a b c : Int}, a โ‰ค b โ†’ b < c โ†’ a < c
Int.lt_of_le_of_lt
H1: 0 โ‰ค a
H1
H2: a < b
H2
) with | _, _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.16838} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.16842} {a : ฮฑ}, a = a
rfl
โŸฉ =>
congrArg: โˆ€ {ฮฑ : Sort ?u.16940} {ฮฒ : Sort ?u.16939} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
Nat.cast: {R : Type ?u.16945} โ†’ [inst : NatCast R] โ†’ Nat โ†’ R
Nat.cast
<|
Nat.div_eq_of_lt: โˆ€ {a b : Nat}, a < b โ†’ a / b = 0
Nat.div_eq_of_lt
<|
ofNat_lt: โˆ€ {n m : Nat}, โ†‘n < โ†‘m โ†” n < m
ofNat_lt
.
1: โˆ€ {a b : Prop}, (a โ†” b) โ†’ a โ†’ b
1
H2: โ†‘wโœยน < โ†‘(succ wโœ)
H2
theorem
add_mul_ediv_right: โˆ€ (a b : Int) {c : Int}, c โ‰  0 โ†’ (a + b * c) / c = a / c + b
add_mul_ediv_right
(
a: Int
a
b: Int
b
:
Int: Type
Int
) {
c: Int
c
:
Int: Type
Int
} (
H: c โ‰  0
H
:
c: Int
c
โ‰ 
0: ?m.17380
0
) : (
a: Int
a
+
b: Int
b
*
c: Int
c
) /
c: Int
c
=
a: Int
a
/
c: Int
c
+
b: Int
b
:= suffices โˆ€ {{
a: Int
a
b: Int
b
c: Int
c
:
Int: Type
Int
}},
0: ?m.17552
0
<
c: Int
c
โ†’ (
a: Int
a
+
b: Int
b
*
c: Int
c
).
ediv: Int โ†’ Int โ†’ Int
ediv
c: Int
c
=
a: Int
a
.
ediv: Int โ†’ Int โ†’ Int
ediv
c: Int
c
+
b: Int
b
from match
Int.lt_trichotomy: โˆ€ (a b : Int), a < b โˆจ a = b โˆจ b < a
Int.lt_trichotomy
c: Int
c
0: ?m.19295
0
with |
Or.inl: โˆ€ {a b : Prop}, a โ†’ a โˆจ b
Or.inl
hlt: c < 0
hlt
=>

Goals accomplished! ๐Ÿ™
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / c = a / c + b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / c = a / c + b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


-((a + b * c) / c) = -(a / c + b)
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / c = a / c + b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / -c = -(a / c + b)
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / c = a / c + b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / -c = -(a / c) + -b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / c = a / c + b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / -c = a / -c + -b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / c = a / c + b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + -b * -c) / -c = a / -c + -b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + -b * -c) / -c = a / -c + -b
a, b, c: Int

H: c โ‰  0

this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b

hlt: c < 0


(a + b * c) / c = a / c + b

Goals accomplished! ๐Ÿ™
|
Or.inr: โˆ€ {a b : Prop}, b โ†’ a โˆจ b
Or.inr
(
Or.inl: โˆ€ {a b : Prop}, a โ†’ a โˆจ b
Or.inl
HEq: c = 0
HEq
) =>
absurd: โˆ€ {a : Prop} {b : Sort ?u.19344}, a โ†’ ยฌa โ†’ b
absurd
HEq: c = 0
HEq
H: c โ‰  0
H
|
Or.inr: โˆ€ {a b : Prop}, b โ†’ a โˆจ b
Or.inr
(
Or.inr: โˆ€ {a b : Prop}, b โ†’ a โˆจ b
Or.inr
hgt: 0 < c
hgt
) =>
this: โˆ€ โฆƒa b c : Intโฆ„, 0 < c โ†’ ediv (a + b * c) c = ediv a c + b
this
hgt: 0 < c
hgt
suffices โˆ€ {
k: Nat
k
n: Nat
n
:
Nat: Type
Nat
} {
a: Int
a
:
Int: Type
Int
}, (
a: Int
a
+
n: Nat
n
*
k: Nat
k
.
succ: Nat โ†’ Nat
succ
).
ediv: Int โ†’ Int โ†’ Int
ediv
k: Nat
k
.
succ: Nat โ†’ Nat
succ
=
a: Int
a
.
ediv: Int โ†’ Int โ†’ Int
ediv
k: Nat
k
.
succ: Nat โ†’ Nat
succ
+
n: Nat
n
from fun
a: ?m.18068
a
b: ?m.18071
b
c: ?m.18074
c
H: ?m.18077
H
=> match
c: ?m.18074
c
,
eq_succ_of_zero_lt: โˆ€ {a : Int}, 0 < a โ†’ โˆƒ n, a = โ†‘(succ n)
eq_succ_of_zero_lt
H: ?m.18077
H
,
b: ?m.18071
b
with | _, โŸจ
_: Nat
_
,
rfl: โˆ€ {ฮฑ : Sort ?u.18106} {a : ฮฑ}, a = a
rfl
โŸฉ,
ofNat: Nat โ†’ Int
ofNat
_ =>
this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n
this
| _, โŸจ
k: Nat
k
,
rfl: โˆ€ {ฮฑ : Sort ?u.18181} {a : ฮฑ}, a = a
rfl
โŸฉ, -[
n: Nat
n
+1] => show (
a: ?m.18068
a
-
n: Nat
n
.
succ: Nat โ†’ Nat
succ
*
k: Nat
k
.
succ: Nat โ†’ Nat
succ
).
ediv: Int โ†’ Int โ†’ Int
ediv
k: Nat
k
.
succ: Nat โ†’ Nat
succ
=
a: ?m.18068
a
.
ediv: Int โ†’ Int โ†’ Int
ediv
k: Nat
k
.
succ: Nat โ†’ Nat
succ
-
n: Nat
n
.
succ: Nat โ†’ Nat
succ
by
aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


ediv (a - โ†‘(succ n) * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) - โ†‘(succ n)
aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


ediv (a - โ†‘(succ n) * โ†‘(succ k)) โ†‘(succ k) + ?m.22475 - ?m.22475 = ediv a โ†‘(succ k) - โ†‘(succ n)
aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


ediv (a - โ†‘(succ n) * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) - โ†‘(succ n)
aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


ediv (a - โ†‘(succ n) * โ†‘(succ k) + โ†‘?m.22482 * โ†‘(succ k)) โ†‘(succ k) - โ†‘?m.22482 = ediv a โ†‘(succ k) - โ†‘(succ n)
aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


ediv (a - โ†‘(succ n) * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) - โ†‘(succ n)
aโœ, bโœ, cโœ: Int

Hโœ: cโœ โ‰  0

this: โˆ€ {k n : Nat} {a : Int}, ediv (a + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv a โ†‘(succ k) + โ†‘n

a, b, c: Int

k, n: Nat

H: 0 < โ†‘(succ k)


ediv a โ†‘(succ k) - โ†‘(succ n) = ediv a โ†‘(succ k) - โ†‘(succ n)

Goals accomplished! ๐Ÿ™
fun {
k: ?m.17858
k
n: ?m.17861
n
} => @fun |
ofNat: Nat โ†’ Int
ofNat
m: Nat
m
=>
congrArg: โˆ€ {ฮฑ : Sort ?u.17877} {ฮฒ : Sort ?u.17876} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
ofNat: Nat โ†’ Int
ofNat
<|
Nat.add_mul_div_right: โˆ€ (x y : Nat) {z : Nat}, 0 < z โ†’ (x + y * z) / z = x / z + y
Nat.add_mul_div_right
_: Nat
_
_: Nat
_
k: ?m.17858
k
.
succ_pos: โˆ€ (n : Nat), 0 < succ n
succ_pos
| -[
m: Nat
m
+1] =>

Goals accomplished! ๐Ÿ™
a, b, c: Int

H: c โ‰  0

k, n, m: Nat


ediv (-[m+1] + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv -[m+1] โ†‘(succ k) + โ†‘n
a, b, c: Int

H: c โ‰  0

k, n, m: Nat


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat


ediv (-[m+1] + โ†‘n * โ†‘(succ k)) โ†‘(succ k) = ediv -[m+1] โ†‘(succ k) + โ†‘n
a, b, c: Int

H: c โ‰  0

k, n, m: Nat


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv โ†‘(n * succ k - succ m) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv โ†‘(n * succ k - succ m) โ†‘(succ k) = โ†‘(n - succ (m / succ k))
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv โ†‘(n * succ k - succ m) โ†‘(succ k) = โ†‘(n - succ (m / succ k))
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


(n * succ k - succ m) / succ k = n - succ (m / succ k)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


(n * succ k - succ m) / succ k = n - succ (m / succ k)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


(succ k * n - succ m) / succ k = n - succ (m / succ k)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


(n * succ k - succ m) / succ k = n - succ (m / succ k)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


n - succ (m / succ k) = n - succ (m / succ k)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


hโ‚
m < succ k * n
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


hโ‚
m < succ k * n
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


hโ‚
m < succ k * n
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


hโ‚
m < succ k * n
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


hโ‚
m < n * succ k
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: m < n * succ k


hโ‚
m < n * succ k
a, b, c: Int

H: c โ‰  0

k, n, m: Nat


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: ยฌm < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: ยฌm < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)

Goals accomplished! ๐Ÿ™
aโœ, bโœ, c: Int

H: c โ‰  0

k, n, m: Nat

hโœยน: ยฌm < n * succ k

hโœ: n * succ k โ‰ค m

a, b: Nat

h: a โ‰ค b


โ†‘a + -(โ†‘b + 1) = -[b - a+1]
aโœ, bโœ, c: Int

H: c โ‰  0

k, n, m: Nat

hโœยน: ยฌm < n * succ k

hโœ: n * succ k โ‰ค m

a, b: Nat

h: a โ‰ค b


โ†‘a + -(โ†‘b + 1) = -[b - a+1]
aโœ, bโœ, c: Int

H: c โ‰  0

k, n, m: Nat

hโœยน: ยฌm < n * succ k

hโœ: n * succ k โ‰ค m

a, b: Nat

h: a โ‰ค b


โ†‘a + -(โ†‘b + 1) = -(โ†‘(b - a) + 1)
aโœ, bโœ, c: Int

H: c โ‰  0

k, n, m: Nat

hโœยน: ยฌm < n * succ k

hโœ: n * succ k โ‰ค m

a, b: Nat

h: a โ‰ค b


โ†‘a + -(โ†‘b + 1) = -[b - a+1]
aโœ, bโœ, c: Int

H: c โ‰  0

k, n, m: Nat

hโœยน: ยฌm < n * succ k

hโœ: n * succ k โ‰ค m

a, b: Nat

h: a โ‰ค b


โ†‘a + -(โ†‘b + 1) = -(โ†‘b - โ†‘a + 1)
aโœ, bโœ, c: Int

H: c โ‰  0

k, n, m: Nat

hโœยน: ยฌm < n * succ k

hโœ: n * succ k โ‰ค m

a, b: Nat

h: a โ‰ค b


โ†‘a + -(โ†‘b + 1) = -(โ†‘b - โ†‘a + 1)
aโœ, bโœ, c: Int

H: c โ‰  0

k, n, m: Nat

hโœยน: ยฌm < n * succ k

hโœ: n * succ k โ‰ค m

a, b: Nat

h: a โ‰ค b


โ†‘a + -(โ†‘b + 1) = -[b - a+1]

Goals accomplished! ๐Ÿ™
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: ยฌm < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


ediv (โ†‘(n * succ k) + -(โ†‘m + 1)) โ†‘(succ k) = โ†‘n + -(โ†‘(m / succ k) + 1)
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: ยฌm < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


ediv (โ†‘(n * succ k) + -(โ†‘m + 1)) โ†‘(succ k) = โ†‘n + -(โ†‘(m / succ k) + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


ediv -[m - n * succ k+1] โ†‘(succ k) = โ†‘n + -(โ†‘(m / succ k) + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


ediv (โ†‘(n * succ k) + -(โ†‘m + 1)) โ†‘(succ k) = โ†‘n + -(โ†‘(m / succ k) + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


ediv -[m - n * succ k+1] โ†‘(succ k) = -[m / succ k - n+1]
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


ediv -[m - n * succ k+1] โ†‘(succ k) = -[m / succ k - n+1]
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: ยฌm < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


(m - n * succ k) / succ k = m / succ k - n
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: ยฌm < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


(m - n * succ k) / succ k = m / succ k - n
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


(m - succ k * n) / succ k = m / succ k - n
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


(m - n * succ k) / succ k = m / succ k - n
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


m / succ k - n = m / succ k - n
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


hโ‚
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


hโ‚
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


hโ‚
a, b, c: Int

H: c โ‰  0

k, n, m: Nat

h: ยฌm < n * succ k


ediv (โ†‘(n * succ k) - โ†‘(succ m)) โ†‘(succ k) = โ†‘n - โ†‘(m / succ k + 1)
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


hโ‚
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


hโ‚
a, b, c: Int

Hโœ: c โ‰  0

k, n, m: Nat

hโœ: ยฌm < n * succ k

h: n * succ k โ‰ค m

H: โˆ€ {a b : Nat}, a โ‰ค b โ†’ โ†‘a + -(โ†‘b + 1) = -[b - a+1]


hโ‚
theorem
add_mul_ediv_left: โˆ€ (a : Int) {b : Int} (c : Int), b โ‰  0 โ†’ (a + b * c) / b = a / b + c
add_mul_ediv_left
(
a: Int
a
:
Int: Type
Int
) {
b: Int
b
:
Int: Type
Int
} (
c: Int
c
:
Int: Type
Int
) (
H: b โ‰  0
H
:
b: Int
b
โ‰ 
0: ?m.22707
0
) : (
a: Int
a
+
b: Int
b
*
c: Int
c
) /
b: Int
b
=
a: Int
a
/
b: Int
b
+
c: Int
c
:=
Int.mul_comm: โˆ€ (a b : Int), a * b = b * a
Int.mul_comm
.. โ–ธ
Int.add_mul_ediv_right: โˆ€ (a b : Int) {c : Int}, c โ‰  0 โ†’ (a + b * c) / c = a / c + b
Int.add_mul_ediv_right
_: Int
_
_: Int
_
H: b โ‰  0
H
theorem
add_ediv_of_dvd_right: โˆ€ {a b c : Int}, c โˆฃ b โ†’ (a + b) / c = a / c + b / c
add_ediv_of_dvd_right
{
a: Int
a
b: Int
b
c: Int
c
:
Int: Type
Int
} (
H: c โˆฃ b
H
:
c: Int
c
โˆฃ
b: Int
b
) : (
a: Int
a
+
b: Int
b
) /
c: Int
c
=
a: Int
a
/
c: Int
c
+
b: Int
b
/
c: Int
c
:= if
h: ?m.23104
h
:
c: Int
c
=
0: ?m.23066
0
then

Goals accomplished! ๐Ÿ™
a, b, c: Int

H: c โˆฃ b

h: c = 0


(a + b) / c = a / c + b / c

Goals accomplished! ๐Ÿ™
else

Goals accomplished! ๐Ÿ™
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + c * k) / c = a / c + c * k / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + k * c) / c = a / c + k * c / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


a / c + k = a / c + k * c / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


a / c + k = a / c + (0 + k * c) / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


a / c + k = a / c + (0 / c + k)
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


a / c + k = a / c + (0 + k)
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ b

h: ยฌc = 0

k: Int

hk: b = c * k


a / c + k = a / c + k

Goals accomplished! ๐Ÿ™
theorem
add_ediv_of_dvd_left: โˆ€ {a b c : Int}, c โˆฃ a โ†’ (a + b) / c = a / c + b / c
add_ediv_of_dvd_left
{
a: Int
a
b: Int
b
c: Int
c
:
Int: Type
Int
} (
H: c โˆฃ a
H
:
c: Int
c
โˆฃ
a: Int
a
) : (
a: Int
a
+
b: Int
b
) /
c: Int
c
=
a: Int
a
/
c: Int
c
+
b: Int
b
/
c: Int
c
:=

Goals accomplished! ๐Ÿ™
a, b, c: Int

H: c โˆฃ a


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ a


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ a


(b + a) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ a


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ a


b / c + a / c = a / c + b / c
a, b, c: Int

H: c โˆฃ a


(a + b) / c = a / c + b / c
a, b, c: Int

H: c โˆฃ a


a / c + b / c = a / c + b / c

Goals accomplished! ๐Ÿ™
@[simp] theorem
mul_ediv_cancel: โˆ€ (a : Int) {b : Int}, b โ‰  0 โ†’ a * b / b = a
mul_ediv_cancel
(
a: Int
a
:
Int: Type
Int
) {
b: Int
b
:
Int: Type
Int
} (
H: b โ‰  0
H
:
b: Int
b
โ‰ 
0: ?m.23851
0
) : (
a: Int
a
*
b: Int
b
) /
b: Int
b
=
a: Int
a
:=

Goals accomplished! ๐Ÿ™
a, b: Int

H: b โ‰  0


a * b / b = a
a, b: Int

H: b โ‰  0

this: (0 + a * b) / b = 0 / b + a


a * b / b = a
a, b: Int

H: b โ‰  0


a * b / b = a
a, b: Int

H: b โ‰  0

this: (0 + a * b) / b = 0 / b + a


a * b / b = a
a, b: Int

H: b โ‰  0

this: a * b / b = 0 / b + a


a * b / b = a
a, b: Int

H: b โ‰  0

this: (0 + a * b) / b = 0 / b + a


a * b / b = a
a, b: Int

H: b โ‰  0

this: a * b / b = 0 + a


a * b / b = a
a, b: Int

H: b โ‰  0

this: (0 + a * b) / b = 0 / b + a


a * b / b = a
a, b: Int

H: b โ‰  0

this: a * b / b = a


a * b / b = a
a, b: Int

H: b โ‰  0

this: a * b / b = a


a * b / b = a

Goals accomplished! ๐Ÿ™
@[simp] theorem
mul_fdiv_cancel: โˆ€ (a : Int) {b : Int}, b โ‰  0 โ†’ fdiv (a * b) b = a
mul_fdiv_cancel
(
a: Int
a
:
Int: Type
Int
) {
b: Int
b
:
Int: Type
Int
} (
H: b โ‰  0
H
:
b: Int
b
โ‰ 
0: ?m.24066
0
) :
fdiv: Int โ†’ Int โ†’ Int
fdiv
(
a: Int
a
*
b: Int
b
)
b: Int
b
=
a: Int
a
:= if
b0: ?m.24158
b0
:
0: ?m.24118
0
โ‰ค
b: Int
b
then

Goals accomplished! ๐Ÿ™
a, b: Int

H: b โ‰  0

b0: 0 โ‰ค b


fdiv (a * b) b = a
a, b: Int

H: b โ‰  0

b0: 0 โ‰ค b


fdiv (a * b) b = a
a, b: Int

H: b โ‰  0

b0: 0 โ‰ค b


a * b / b = a
a, b: Int

H: b โ‰  0

b0: 0 โ‰ค b


fdiv (a * b) b = a
a, b: Int

H: b โ‰  0

b0: 0 โ‰ค b


a = a

Goals accomplished! ๐Ÿ™
else match
a: Int
a
,
b: Int
b
,
Int.not_le: โˆ€ {a b : Int}, ยฌa โ‰ค b โ†” b < a
Int.not_le
.
1: โˆ€ {a b : Prop}, (a โ†” b) โ†’ a โ†’ b
1
b0: ?m.24158
b0
with |
0: Int
0
, _, _ =>

Goals accomplished! ๐Ÿ™
a, b, xโœยน: Int

xโœ: xโœยน < 0

H: xโœยน โ‰  0

b0: ยฌ0 โ‰ค xโœยน


fdiv (0 * xโœยน) xโœยน = 0

Goals accomplished! ๐Ÿ™
|
succ: Nat โ†’ Nat
succ
a: Nat
a
, -[
b: Nat
b
+1], _ =>
congrArg: โˆ€ {ฮฑ : Sort ?u.24313} {ฮฒ : Sort ?u.24312} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
ofNat: Nat โ†’ Int
ofNat
<|
Nat.mul_div_cancel: โˆ€ (m : Nat) {n : Nat}, 0 < n โ†’ m * n / n = m
Nat.mul_div_cancel
(
succ: Nat โ†’ Nat
succ
a: Nat
a
)
b: Nat
b
.
succ_pos: โˆ€ (n : Nat), 0 < succ n
succ_pos
| -[
a: Nat
a
+1], -[
b: Nat
b
+1], _ =>
congrArg: โˆ€ {ฮฑ : Sort ?u.24622} {ฮฒ : Sort ?u.24621} {aโ‚ aโ‚‚ : ฮฑ} (f : ฮฑ โ†’ ฮฒ), aโ‚ = aโ‚‚ โ†’ f aโ‚ = f aโ‚‚
congrArg
negSucc: Nat โ†’ Int
negSucc
<|
Nat.div_eq_of_lt_le: โˆ€ {k n m : Nat}, k * n โ‰ค m โ†’ m < succ k * n โ†’ m / n = k
Nat.div_eq_of_lt_le
(
le_of_lt_succ: โˆ€ {m n : Nat}, m < succ n โ†’ m โ‰ค n
le_of_lt_succ
<|
Nat.mul_lt_mul_of_pos_right: โˆ€ {n m k : Nat}, n < m โ†’ k > 0 โ†’ n * k < m * k
Nat.mul_lt_mul_of_pos_right
a: Nat
a
.
lt_succ_self: โˆ€ (n : Nat), n < succ n
lt_succ_self
b: Nat
b
.
succ_pos: โˆ€ (n : Nat), 0 < succ n
succ_pos
) (
lt_succ_self: โˆ€ (n : Nat), n < succ n
lt_succ_self
_: Nat
_
) @[simp] protected theorem
mul_div_cancel: โˆ€ (a : Int) {b : Int}, b โ‰  0 โ†’ div (a * b) b = a
mul_div_cancel
(
a: Int
a
:
Int: Type
Int
) {
b: Int
b
:
Int: Type
Int
} (
H: b โ‰  0
H
:
b: Int
b
โ‰ 
0: ?m.25516
0
) : (
a: Int
a
*
b: Int
b
).
div: Int โ†’ Int โ†’ Int
div
b: Int
b
=
a: Int
a
:= have : โˆ€ {
a: Nat
a
b: Nat
b
:
Nat: Type
Nat
}, (
b: Nat
b
:
Int: Type
Int
) โ‰ 
0: ?m.25613
0
โ†’ (
div: Int โ†’ Int โ†’ Int
div
(
a: Nat
a
*
b: Nat
b
)
b: Nat
b
:
Int: Type
Int
) =
a: Nat
a
:= fun
H: ?m.25803
H
=>

Goals accomplished! ๐Ÿ™
a, b: Int

Hโœ: b โ‰  0

aโœ, bโœ: Nat

H: โ†‘bโœ โ‰  0


div (โ†‘aโœ * โ†‘bโœ) โ†‘bโœ = โ†‘aโœ
a, b: Int

Hโœ: b โ‰  0

aโœ, bโœ: Nat

H: โ†‘bโœ โ‰  0


div (โ†‘aโœ * โ†‘bโœ) โ†‘bโœ = โ†‘aโœ
a, b: Int

Hโœ: b โ‰  0

aโœ, bโœ: Nat

H: โ†‘bโœ โ‰  0


div โ†‘(aโœ * bโœ) โ†‘bโœ = โ†‘aโœ
a, b: Int

Hโœ: b โ‰  0

aโœ, bโœ: Nat

H: โ†‘bโœ โ‰  0


div (โ†‘aโœ * โ†‘bโœ) โ†‘bโœ = โ†‘aโœ
a, b: Int

Hโœ: b โ‰  0

aโœ, bโœ: Nat

H: โ†‘bโœ โ‰  0


โ†‘(aโœ * bโœ / bโœ) = โ†‘aโœ
a, b: Int

Hโœ: b โ‰  0

aโœ, bโœ: Nat

H: โ†‘bโœ โ‰  0


div (โ†‘aโœ * โ†‘bโœ) โ†‘bโœ = โ†‘aโœ
a, b: Int

Hโœ: b โ‰  0

aโœ, bโœ: Nat

H: โ†‘bโœ โ‰  0


โ†‘aโœ = โ†‘aโœ

Goals accomplished! ๐Ÿ™
match
a: Int
a
,
b: Int
b
,
a: Int
a
.
eq_nat_or_neg: โˆ€ (a : Int), โˆƒ n, a = โ†‘n โˆจ a = -โ†‘n
eq_nat_or_neg
,
b: Int
b
.
eq_nat_or_neg: โˆ€ (a : Int), โˆƒ n, a = โ†‘n โˆจ a = -โ†‘n
eq_nat_or_neg
with | _, _, โŸจ
a: Nat
a
,
.inl: โˆ€ {a b : Prop}, a โ†’ a โˆจ b
.inl
rfl: โˆ€ {ฮฑ : Sort ?u.25840} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
b: Nat
b
,
.inl: โˆ€ {a b : Prop}, a โ†’ a โˆจ b
.inl
rfl: โˆ€ {ฮฑ : Sort ?u.25844} {a : ฮฑ}, a = a
rfl
โŸฉ =>
this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a
this
H: โ†‘b โ‰  0
H
| _, _, โŸจ
a: Nat
a
,
.inl: โˆ€ {a b : Prop}, a โ†’ a โˆจ b
.inl
rfl: โˆ€ {ฮฑ : Sort ?u.25983} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
b: Nat
b
,
.inr: โˆ€ {a b : Prop}, b โ†’ a โˆจ b
.inr
rfl: โˆ€ {ฮฑ : Sort ?u.25987} {a : ฮฑ}, a = a
rfl
โŸฉ =>

Goals accomplished! ๐Ÿ™
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * -โ†‘b) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * -โ†‘b) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (-(โ†‘a * โ†‘b)) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * -โ†‘b) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


-div (โ†‘a * โ†‘b) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * -โ†‘b) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


- -div (โ†‘a * โ†‘b) โ†‘b = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * -โ†‘b) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * โ†‘b) โ†‘b = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * -โ†‘b) (-โ†‘b) = โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


โ†‘a = โ†‘a

Goals accomplished! ๐Ÿ™
| _, _, โŸจ
a: Nat
a
,
.inr: โˆ€ {a b : Prop}, b โ†’ a โˆจ b
.inr
rfl: โˆ€ {ฮฑ : Sort ?u.26066} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
b: Nat
b
,
.inl: โˆ€ {a b : Prop}, a โ†’ a โˆจ b
.inl
rfl: โˆ€ {ฮฑ : Sort ?u.26070} {a : ฮฑ}, a = a
rfl
โŸฉ =>

Goals accomplished! ๐Ÿ™
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: โ†‘b โ‰  0


div (-โ†‘a * โ†‘b) โ†‘b = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: โ†‘b โ‰  0


div (-โ†‘a * โ†‘b) โ†‘b = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: โ†‘b โ‰  0


div (-(โ†‘a * โ†‘b)) โ†‘b = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: โ†‘b โ‰  0


div (-โ†‘a * โ†‘b) โ†‘b = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: โ†‘b โ‰  0


-div (โ†‘a * โ†‘b) โ†‘b = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: โ†‘b โ‰  0


div (-โ†‘a * โ†‘b) โ†‘b = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: โ†‘b โ‰  0


-โ†‘a = -โ†‘a

Goals accomplished! ๐Ÿ™
| _, _, โŸจ
a: Nat
a
,
.inr: โˆ€ {a b : Prop}, b โ†’ a โˆจ b
.inr
rfl: โˆ€ {ฮฑ : Sort ?u.26149} {a : ฮฑ}, a = a
rfl
โŸฉ, โŸจ
b: Nat
b
,
.inr: โˆ€ {a b : Prop}, b โ†’ a โˆจ b
.inr
rfl: โˆ€ {ฮฑ : Sort ?u.26153} {a : ฮฑ}, a = a
rfl
โŸฉ =>

Goals accomplished! ๐Ÿ™
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (-โ†‘a * -โ†‘b) (-โ†‘b) = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (-โ†‘a * -โ†‘b) (-โ†‘b) = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (โ†‘a * โ†‘b) (-โ†‘b) = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (-โ†‘a * -โ†‘b) (-โ†‘b) = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


-div (โ†‘a * โ†‘b) โ†‘b = -โ†‘a
aโœ, bโœ: Int

this: โˆ€ {a b : Nat}, โ†‘b โ‰  0 โ†’ div (โ†‘a * โ†‘b) โ†‘b = โ†‘a

a, b: Nat

H: -โ†‘b โ‰  0


div (-โ†‘a * -โ†‘b) (-โ†‘b) = -โ†‘a