feat: port Data.Fin.Basic (#1084)

mathlib3 SHA: 0bd2ea37bcba5769e14866170f251c9bc64e35d7



Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/Data/ByteArray.lean

@@ -2,6 +2,23 @@ import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Char
 import Mathlib.Data.UInt
 
+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
+
 /-- A terminal byte slice, a suffix of a byte array. -/
 structure ByteSliceT := (arr : ByteArray) (off : Nat)