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) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/

namespace Fin

@[simp] theorem 
ofNat'_zero_val: βˆ€ {a : Nat} {h : a > 0}, (Fin.ofNat' 0 h).val = 0
ofNat'_zero_val : (
Fin.ofNat': {n : Nat} β†’ Nat β†’ n > 0 β†’ Fin n
Fin.ofNat' 
0: ?m.20
0 
h: ?m.14
h).
val: {n : Nat} β†’ Fin n β†’ Nat
val = 
0: ?m.31
0 := 
Nat.zero_mod: βˆ€ (b : Nat), 0 % b = 0
Nat.zero_mod 
_: Nat
_

@[simp] theorem 
mod_val: βˆ€ {n : Nat} (a b : Fin n), (a % b).val = a.val % b.val
mod_val (
a: Fin n
a 
b: Fin n
b : 
Fin: Nat β†’ Type
Fin 
n: ?m.73
n) : (
a: Fin n
a % 
b: Fin n
b).
val: {n : Nat} β†’ Fin n β†’ Nat
val = 
a: Fin n
a.
val: {n : Nat} β†’ Fin n β†’ Nat
val % 
b: Fin n
b.
val: {n : Nat} β†’ Fin n β†’ Nat
val :=
  
Nat.mod_eq_of_lt: βˆ€ {a b : Nat}, a < b β†’ a % b = a
Nat.mod_eq_of_lt (
Nat.lt_of_le_of_lt: βˆ€ {n m k : Nat}, n ≀ m β†’ m < k β†’ n < k
Nat.lt_of_le_of_lt (
Nat.mod_le: βˆ€ (x y : Nat), x % y ≀ x
Nat.mod_le ..) 
a: Fin n
a.
2: βˆ€ {n : Nat} (self : Fin n), self.val < n
2)

@[simp] theorem 
div_val: βˆ€ {n : Nat} (a b : Fin n), (a / b).val = a.val / b.val
div_val (
a: Fin n
a 
b: Fin n
b : 
Fin: Nat β†’ Type
Fin 
n: ?m.204
n) : (
a: Fin n
a / 
b: Fin n
b).
val: {n : Nat} β†’ Fin n β†’ Nat
val = 
a: Fin n
a.
val: {n : Nat} β†’ Fin n β†’ Nat
val / 
b: Fin n
b.
val: {n : Nat} β†’ Fin n β†’ Nat
val :=
  
Nat.mod_eq_of_lt: βˆ€ {a b : Nat}, a < b β†’ a % b = a
Nat.mod_eq_of_lt (
Nat.lt_of_le_of_lt: βˆ€ {n m k : Nat}, n ≀ m β†’ m < k β†’ n < k
Nat.lt_of_le_of_lt (
Nat.div_le_self: βˆ€ (n k : Nat), n / k ≀ n
Nat.div_le_self ..) 
a: Fin n
a.
2: βˆ€ {n : Nat} (self : Fin n), self.val < n
2)

@[simp] theorem 
modn_val: βˆ€ {n : Nat} (a : Fin n) (b : Nat), (modn a b).val = a.val % b
modn_val (
a: Fin n
a : 
Fin: Nat β†’ Type
Fin 
n: ?m.341
n) (
b: Nat
b : 
Nat: Type
Nat) : (
a: Fin n
a.
modn: {n : Nat} β†’ Fin n β†’ Nat β†’ Fin n
modn 
b: Nat
b).
val: {n : Nat} β†’ Fin n β†’ Nat
val = 
a: Fin n
a.
val: {n : Nat} β†’ Fin n β†’ Nat
val % 
b: Nat
b :=
  
Nat.mod_eq_of_lt: βˆ€ {a b : Nat}, a < b β†’ a % b = a
Nat.mod_eq_of_lt (
Nat.lt_of_le_of_lt: βˆ€ {n m k : Nat}, n ≀ m β†’ m < k β†’ n < k
Nat.lt_of_le_of_lt (
Nat.mod_le: βˆ€ (x y : Nat), x % y ≀ x
Nat.mod_le ..) 
a: Fin n
a.
2: βˆ€ {n : Nat} (self : Fin n), self.val < n
2)

end Fin

namespace USize

@[simp] theorem 
lt_def: βˆ€ {a b : USize}, a < b ↔ toNat a < toNat b
lt_def {
a: USize
a 
b: USize
b : 
USize: Type
USize} : 
a: USize
a < 
b: USize
b ↔ 
a: USize
a.
toNat: USize β†’ Nat
toNat < 
b: USize
b.
toNat: USize β†’ Nat
toNat := 
.rfl: βˆ€ {a : Prop}, a ↔ a
.rfl

@[simp] theorem 
le_def: βˆ€ {a b : USize}, a ≀ b ↔ toNat a ≀ toNat b
le_def {
a: USize
a 
b: USize
b : 
USize: Type
USize} : 
a: USize
a ≀ 
b: USize
b ↔ 
a: USize
a.
toNat: USize β†’ Nat
toNat ≀ 
b: USize
b.
toNat: USize β†’ Nat
toNat := 
.rfl: βˆ€ {a : Prop}, a ↔ a
.rfl

@[simp] theorem 
zero_toNat: toNat 0 = 0
zero_toNat : (
0: ?m.524
0 : 
USize: Type
USize).
toNat: USize β†’ Nat
toNat = 
0: ?m.534
0 := 
Nat.zero_mod: βˆ€ (b : Nat), 0 % b = 0
Nat.zero_mod 
_: Nat
_

@[simp] theorem 
mod_toNat: βˆ€ (a b : USize), toNat (a % b) = toNat a % toNat b
mod_toNat (
a: USize
a 
b: USize
b : 
USize: Type
USize) : (
a: USize
a % 
b: USize
b).
toNat: USize β†’ Nat
toNat = 
a: USize
a.
toNat: USize β†’ Nat
toNat % 
b: USize
b.
toNat: USize β†’ Nat
toNat :=
  
Fin.mod_val: βˆ€ {n : Nat} (a b : Fin n), (a % b).val = a.val % b.val
Fin.mod_val ..

@[simp] theorem 
div_toNat: βˆ€ (a b : USize), toNat (a / b) = toNat a / toNat b
div_toNat (
a: USize
a 
b: USize
b : 
USize: Type
USize) : (
a: USize
a / 
b: USize
b).
toNat: USize β†’ Nat
toNat = 
a: USize
a.
toNat: USize β†’ Nat
toNat / 
b: USize
b.
toNat: USize β†’ Nat
toNat :=
  
Fin.div_val: βˆ€ {n : Nat} (a b : Fin n), (a / b).val = a.val / b.val
Fin.div_val ..

@[simp] theorem 
modn_toNat: βˆ€ (a : USize) (b : Nat), toNat (modn a b) = toNat a % b
modn_toNat (
a: USize
a : 
USize: Type
USize) (
b: Nat
b : 
Nat: Type
Nat) : (
a: USize
a.
modn: USize β†’ Nat β†’ USize
modn 
b: Nat
b).
toNat: USize β†’ Nat
toNat = 
a: USize
a.
toNat: USize β†’ Nat
toNat % 
b: Nat
b :=
  
Fin.modn_val: βˆ€ {n : Nat} (a : Fin n) (b : Nat), (Fin.modn a b).val = a.val % b
Fin.modn_val ..

theorem 
mod_lt: βˆ€ (a b : USize), 0 < b β†’ a % b < b
mod_lt (
a: USize
a 
b: USize
b : 
USize: Type
USize) (
h: 0 < b
h : 
0: ?m.884
0 < 
b: USize
b) : 
a: USize
a % 
b: USize
b < 
b: USize
b := 
USize.modn_lt: βˆ€ {m : Nat} (u : USize), m > 0 β†’ toNat (u % m) < m
USize.modn_lt 
_: USize
_ (
Goals accomplished! πŸ™
a, b: USize

h: 0 < b

b.1.val > 0
a, b: USize

h: 0 < toNat b

b.1.val > 0
a, b: USize

h: 0 < toNat b

b.1.val > 0
a, b: USize

h: 0 < b

b.1.val > 0
Goals accomplished! πŸ™
)

theorem 
toNat.inj: βˆ€ {a b : USize}, toNat a = toNat b β†’ a = b
toNat.inj : βˆ€ {
a: USize
a 
b: USize
b : 
USize: Type
USize}, 
a: USize
a.
toNat: USize β†’ Nat
toNat = 
b: USize
b.
toNat: USize β†’ Nat
toNat β†’ 
a: USize
a = 
b: USize
b
  | ⟨
_: Nat
_, 
_: val✝ < size
_⟩, ⟨_, _⟩, 
rfl: βˆ€ {Ξ± : Sort ?u.1081} {a : Ξ±}, a = a
rfl => 
rfl: βˆ€ {Ξ± : Sort ?u.1138} {a : Ξ±}, a = a
rfl

end USize