feat: port Data.Nat.Basic (#729)

This is based on a *future* version of mathlib3, once leanprover-community/mathlib3#17763 and leanprover-community/mathlib3#17759 have landed. - [x] depends on #727 - [x] depends on #730 Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Nov 30, 2022 · 80eed25 · 80eed25
1 parent 8b5a89e
commit 80eed25
Show file tree

Hide file tree

Showing 3 changed files with 979 additions and 19 deletions.
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
@@ -4,6 +4,23 @@ import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.Ring.Basic
 
+namespace Nat
+
+/- Up -/
+
+/-- A well-ordered relation for "upwards" induction on the natural numbers up to some bound `ub`. -/
+def Up (ub a i : ℕ) := i < a ∧ i < ub
+
+lemma Up.next {ub i} (h : i < ub) : Up ub (i+1) i := ⟨Nat.lt_succ_self _, h⟩
+
+lemma Up.WF (ub) : WellFounded (Up ub) :=
+  Subrelation.wf (h₂ := (measure (ub - .)).wf) fun ⟨ia, iu⟩ ↦ Nat.sub_lt_sub_left iu ia
+
+/-- A well-ordered relation for "upwards" induction on the natural numbers up to some bound `ub`. -/
+def upRel (ub : ℕ) : WellFoundedRelation Nat := ⟨Up ub, Up.WF ub⟩
+
+end Nat
+
 instance : Subsingleton (Fin 0) where
   allEq := fun.