m n k : Nat
e : n = m * k
⊢ 0 < n → m ≤ n
m n : Nat
h : 0 < n
k : Nat
e : n = m * k
⊢ m ≤ n
revert h
m n k : Nat
e : n = m * k
⊢ 0 < m * k → m ≤ m * k
m n k : Nat
e : n = m * k
⊢ 0 < n → m ≤ n
rw [e]
no goals
m n k : Nat
e : n = m * k
⊢ 0 < m * k → m ≤ m * k
match k with
| 0 => intro hn; simp at hn
| pk+1 =>
  intro
  have := Nat.mul_le_mul_left m (succ_pos pk)
  rwa [Nat.mul_one] at this
m n k : Nat
e : n = m * 0
hn : 0 < m * 0
⊢ m ≤ m * 0
m n k : Nat
e : n = m * 0
⊢ 0 < m * 0 → m ≤ m * 0
intro hn
no goals
m n k : Nat
e : n = m * 0
hn : 0 < m * 0
⊢ m ≤ m * 0
simp at hn
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
⊢ m ≤ m * (pk + 1)
m n k pk : Nat
e : n = m * (pk + 1)
⊢ 0 < m * (pk + 1) → m ≤ m * (pk + 1)
intro
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
this : m * succ 0 ≤ m * succ pk
⊢ m ≤ m * (pk + 1)
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
⊢ m ≤ m * (pk + 1)
have := Nat.mul_le_mul_left m (succ_pos pk)
no goals
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
this : m * succ 0 ≤ m * succ pk
⊢ m ≤ m * (pk + 1)
rwa [Nat.mul_one] at this