max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add Trans instances for tutorial

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-25 08:50:51 -07:00
parent 5003c74191
commit 795ccf6e2b
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Data/Nat/Basic.lean
View file

@ -196,6 +196,18 @@ protected theorem lt_of_lt_of_le {n m k : Nat} : n < m → m ≤ k → n < k :=
protected theorem lt_of_lt_of_eq {n m k : Nat} : n < m → m = k → n < k :=
fun h₁ h₂ => h₂ ▸ h₁
instance : Trans (. < . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) where
trans := Nat.lt_trans
instance : Trans (. ≤ . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) where
trans := Nat.le_trans
instance : Trans (. < . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) where
trans := Nat.lt_of_lt_of_le
instance : Trans (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) where
trans := Nat.lt_of_le_of_lt
protected theorem le_of_eq {n m : Nat} (p : n = m) : n ≤ m :=
p ▸ Nat.le_refl n