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.
```/-
Authors: Mario Carneiro
-/

namespace Fin

@[simp] theorem ofNat'_zero_val: β {a : Nat} {h : a > 0}, (Fin.ofNat' 0 h).val = 0ofNat'_zero_val : (Fin.ofNat': {n : Nat} β Nat β n > 0 β Fin nFin.ofNat' 0: ?m.200 h: ?m.14h).val: {n : Nat} β Fin n β Natval = 0: ?m.310 := Nat.zero_mod: β (b : Nat), 0 % b = 0Nat.zero_mod _: Nat_

@[simp] theorem mod_val: β {n : Nat} (a b : Fin n), (a % b).val = a.val % b.valmod_val (a: Fin na b: Fin nb : Fin: Nat β TypeFin n: ?m.73n) : (a: Fin na % b: Fin nb).val: {n : Nat} β Fin n β Natval = a: Fin na.val: {n : Nat} β Fin n β Natval % b: Fin nb.val: {n : Nat} β Fin n β Natval :=
Nat.mod_eq_of_lt: β {a b : Nat}, a < b β a % b = aNat.mod_eq_of_lt (Nat.lt_of_le_of_lt: β {n m k : Nat}, n β€ m β m < k β n < kNat.lt_of_le_of_lt (Nat.mod_le: β (x y : Nat), x % y β€ xNat.mod_le ..) a: Fin na.2: β {n : Nat} (self : Fin n), self.val < n2)

@[simp] theorem div_val: β {n : Nat} (a b : Fin n), (a / b).val = a.val / b.valdiv_val (a: Fin na b: Fin nb : Fin: Nat β TypeFin n: ?m.204n) : (a: Fin na / b: Fin nb).val: {n : Nat} β Fin n β Natval = a: Fin na.val: {n : Nat} β Fin n β Natval / b: Fin nb.val: {n : Nat} β Fin n β Natval :=
Nat.mod_eq_of_lt: β {a b : Nat}, a < b β a % b = aNat.mod_eq_of_lt (Nat.lt_of_le_of_lt: β {n m k : Nat}, n β€ m β m < k β n < kNat.lt_of_le_of_lt (Nat.div_le_self: β (n k : Nat), n / k β€ nNat.div_le_self ..) a: Fin na.2: β {n : Nat} (self : Fin n), self.val < n2)

@[simp] theorem modn_val: β {n : Nat} (a : Fin n) (b : Nat), (modn a b).val = a.val % bmodn_val (a: Fin na : Fin: Nat β TypeFin n: ?m.341n) (b: Natb : Nat: TypeNat) : (a: Fin na.modn: {n : Nat} β Fin n β Nat β Fin nmodn b: Natb).val: {n : Nat} β Fin n β Natval = a: Fin na.val: {n : Nat} β Fin n β Natval % b: Natb :=
Nat.mod_eq_of_lt: β {a b : Nat}, a < b β a % b = aNat.mod_eq_of_lt (Nat.lt_of_le_of_lt: β {n m k : Nat}, n β€ m β m < k β n < kNat.lt_of_le_of_lt (Nat.mod_le: β (x y : Nat), x % y β€ xNat.mod_le ..) a: Fin na.2: β {n : Nat} (self : Fin n), self.val < n2)

end Fin

namespace USize

@[simp] theorem lt_def: β {a b : USize}, a < b β toNat a < toNat blt_def {a: USizea b: USizeb : USize: TypeUSize} : a: USizea < b: USizeb β a: USizea.toNat: USize β NattoNat < b: USizeb.toNat: USize β NattoNat := .rfl: β {a : Prop}, a β a.rfl

@[simp] theorem le_def: β {a b : USize}, a β€ b β toNat a β€ toNat ble_def {a: USizea b: USizeb : USize: TypeUSize} : a: USizea β€ b: USizeb β a: USizea.toNat: USize β NattoNat β€ b: USizeb.toNat: USize β NattoNat := .rfl: β {a : Prop}, a β a.rfl

@[simp] theorem zero_toNat: toNat 0 = 0zero_toNat : (0: ?m.5240 : USize: TypeUSize).toNat: USize β NattoNat = 0: ?m.5340 := Nat.zero_mod: β (b : Nat), 0 % b = 0Nat.zero_mod _: Nat_

@[simp] theorem mod_toNat: β (a b : USize), toNat (a % b) = toNat a % toNat bmod_toNat (a: USizea b: USizeb : USize: TypeUSize) : (a: USizea % b: USizeb).toNat: USize β NattoNat = a: USizea.toNat: USize β NattoNat % b: USizeb.toNat: USize β NattoNat :=
Fin.mod_val: β {n : Nat} (a b : Fin n), (a % b).val = a.val % b.valFin.mod_val ..

@[simp] theorem div_toNat: β (a b : USize), toNat (a / b) = toNat a / toNat bdiv_toNat (a: USizea b: USizeb : USize: TypeUSize) : (a: USizea / b: USizeb).toNat: USize β NattoNat = a: USizea.toNat: USize β NattoNat / b: USizeb.toNat: USize β NattoNat :=
Fin.div_val: β {n : Nat} (a b : Fin n), (a / b).val = a.val / b.valFin.div_val ..

@[simp] theorem modn_toNat: β (a : USize) (b : Nat), toNat (modn a b) = toNat a % bmodn_toNat (a: USizea : USize: TypeUSize) (b: Natb : Nat: TypeNat) : (a: USizea.modn: USize β Nat β USizemodn b: Natb).toNat: USize β NattoNat = a: USizea.toNat: USize β NattoNat % b: Natb :=
Fin.modn_val: β {n : Nat} (a : Fin n) (b : Nat), (Fin.modn a b).val = a.val % bFin.modn_val ..

theorem mod_lt: β (a b : USize), 0 < b β a % b < bmod_lt (a: USizea b: USizeb : USize: TypeUSize) (h: 0 < bh : 0: ?m.8840 < b: USizeb) : a: USizea % b: USizeb < b: USizeb := USize.modn_lt: β {m : Nat} (u : USize), m > 0 β toNat (u % m) < mUSize.modn_lt _: USize_ (byGoals accomplished! π a, b: USizeh: 0 < bb.1.val > 0simp at h: 0 < bha, b: USizeh: 0 < toNat bb.1.val > 0;a, b: USizeh: 0 < toNat bb.1.val > 0 a, b: USizeh: 0 < bb.1.val > 0exact h: 0 < toNat bhGoals accomplished! π)

theorem toNat.inj: β {a b : USize}, toNat a = toNat b β a = btoNat.inj : β {a: USizea b: USizeb : USize: TypeUSize}, a: USizea.toNat: USize β NattoNat = b: USizeb.toNat: USize β NattoNat β a: USizea = b: USizeb
| β¨_: Nat_, _: valβ < size_β©, β¨_, _β©, rfl: β {Ξ± : Sort ?u.1081} {a : Ξ±}, a = arfl => rfl: β {Ξ± : Sort ?u.1138} {a : Ξ±}, a = arfl

end USize
```