Theorem: verus_lemma_small_mod (VerusLeanStd/ModInternalsNonlinear.lean)

State before:
x m : ℕ
h : x < m
h' : 0 < m
⊢ ↑x % ↑m = ↑x
Tactic:
have h1 : 0 ≤ (x : Int) := by simp only [Nat.cast_nonneg]
State after:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
⊢ ↑x % ↑m = ↑x

State before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
⊢ ↑x % ↑m = ↑x
Tactic:
have h2 : 0 ≤ (m : Int) := by simp only [Nat.cast_nonneg]
State after:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑x % ↑m = ↑x

State before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑x % ↑m = ↑x
Tactic:
rw [← Int.mod_eq_emod h1 h2, ← Int.ofNat_mod x m]
State after:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑(x % m) = ↑x

State before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑(x % m) = ↑x
Tactic:
exact ((fun a b => (Mathlib.Tactic.Zify.nat_cast_eq a b).mp) x (x % m) (Nat.mod_eq_of_lt h).symm).symm
State after:
no goals

State before:
x m : ℕ
h : x < m
h' : 0 < m
⊢ 0 ≤ ↑x
Tactic:
simp only [Nat.cast_nonneg]
State after:
no goals

State before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
⊢ 0 ≤ ↑m
Tactic:
simp only [Nat.cast_nonneg]
State after:
no goals