Theorem: not_le_mod (LeanMeetup/Exercise02Solutions.lean)

State before:
x n : ℕ
⊢ ¬n + 1 ≤ x % (n + 1)
Tactic:
simp only [not_le, Nat.ge_mod]
State after:
no goals