a b : Int
m n : Nat
H : 0 < ↑(succ n)
⊢ -[m+1] % ↑(succ n) < ↑(succ n)
a b : Int
m n : Nat
H : 0 < ↑(succ n)
⊢ -[m+1] % ↑(succ n) < ↑(succ n)
simp [emod, Int.subNatNat_eq_coe]
no goals
a b : Int
m n : Nat
H : 0 < ↑(succ n)
⊢ -[m+1] % ↑(succ n) < ↑(succ n)
exact Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)