Theorem: Imo1981P3.NatPredicate.reduction (Compfiles/Imo1981P3.lean)

State before:
N m n : ℕ
h1 : NatPredicate N m n
h2 : 1 < n
⊢ NatPredicate N (n - m) m
Tactic:
have : m ≤ n := h1.m_le_n
State after:
N m n : ℕ
h1 : NatPredicate N m n
h2 : 1 < n
this : m ≤ n
⊢ NatPredicate N (n - m) m

State before:
N m n : ℕ
h1 : NatPredicate N m n
h2 : 1 < n
this : m ≤ n
⊢ NatPredicate N (n - m) m
Tactic:
exact mod_cast h1.reduction (mod_cast h2)
State after:
no goals