no goals
a b c : Nat
h₁ : a ≤ b
⊢ a * c ≤ b * c
if hba : b ≤ a then simp [Nat.le_antisymm hba h₁] else
if hc0 : c ≤ 0 then simp [Nat.le_antisymm hc0 (zero_le c), Nat.mul_zero] else
exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_right (Nat.not_le.1 hba) (Nat.not_le.1 hc0))
no goals
a b c : Nat
h₁ : a ≤ b
hba : b ≤ a
⊢ a * c ≤ b * c
simp [Nat.le_antisymm hba h₁]
no goals
a b c : Nat
h₁ : a ≤ b
hba : ¬b ≤ a
⊢ a * c ≤ b * c
if hc0 : c ≤ 0 then simp [Nat.le_antisymm hc0 (zero_le c), Nat.mul_zero] else
exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_right (Nat.not_le.1 hba) (Nat.not_le.1 hc0))
no goals
a b c : Nat
h₁ : a ≤ b
hba : ¬b ≤ a
hc0 : c ≤ 0
⊢ a * c ≤ b * c
simp [Nat.le_antisymm hc0 (zero_le c), Nat.mul_zero]
no goals
a b c : Nat
h₁ : a ≤ b
hba : ¬b ≤ a
hc0 : ¬c ≤ 0
⊢ a * c ≤ b * c
exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_right (Nat.not_le.1 hba) (Nat.not_le.1 hc0))