Theorem: Int.modToNat_le (YatimaStdLib/Int.lean)

State before:
a : Int
n : Nat
⊢ modToNat a (succ n) < succ n
Tactic:
cases a with
| ofNat x => simp only [modToNat_ofNat, x.mod_lt (n.succ_pos)]
| negSucc x =>
  let y := x % n.succ
  have : n.succ - y - 1 ≤ n := by
    have : n.succ - y - 1 = n - y := n.add_sub_add_right 1 y
    rw [this]
    exact n.sub_le y
  exact Nat.lt_succ_of_le this
State after:
no goals

State before:
case ofNat
n x : Nat
⊢ modToNat (ofNat x) (succ n) < succ n
Tactic:
simp only [modToNat_ofNat, x.mod_lt (n.succ_pos)]
State after:
no goals

State before:
case negSucc
n x : Nat
⊢ modToNat -[x+1] (succ n) < succ n
Tactic:
let y := x % n.succ
State after:
case negSucc
n x : Nat
y : Nat := x % succ n
⊢ modToNat -[x+1] (succ n) < succ n

State before:
case negSucc
n x : Nat
y : Nat := x % succ n
⊢ modToNat -[x+1] (succ n) < succ n
Tactic:
have : n.succ - y - 1 ≤ n := by
  have : n.succ - y - 1 = n - y := n.add_sub_add_right 1 y
  rw [this]
  exact n.sub_le y
State after:
case negSucc
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 ≤ n
⊢ modToNat -[x+1] (succ n) < succ n

State before:
case negSucc
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 ≤ n
⊢ modToNat -[x+1] (succ n) < succ n
Tactic:
exact Nat.lt_succ_of_le this
State after:
no goals

State before:
n x : Nat
y : Nat := x % succ n
⊢ succ n - y - 1 ≤ n
Tactic:
have : n.succ - y - 1 = n - y := n.add_sub_add_right 1 y
State after:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ succ n - y - 1 ≤ n

State before:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ succ n - y - 1 ≤ n
Tactic:
rw [this]
State after:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ n - y ≤ n

State before:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ n - y ≤ n
Tactic:
exact n.sub_le y
State after:
no goals