Theorem: le_sub_of_dvd_of_dvd_of_lt (Fl/Lemmas.lean)

State before:
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : n < m
⊢ n ≤ m - k
Tactic:
apply le_tsub_of_add_le_right
State after:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : n < m
⊢ n + k ≤ m

State before:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : n < m
⊢ n + k ≤ m
Tactic:
exact add_le_of_dvd_of_dvd_of_lt h₂ h₁ h₃
State after:
no goals