no goals
a b c : Nat
h₁ : a ≤ b
⊢ c * a ≤ c * b
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.zero_mul] else
exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_left (Nat.not_le.1 hba) (Nat.not_le.1 hc0))
no goals
a b c : Nat
h₁ : a ≤ b
hba : b ≤ a
⊢ c * a ≤ c * b
simp [Nat.le_antisymm hba h₁]
no goals
a b c : Nat
h₁ : a ≤ b
hba : ¬b ≤ a
⊢ c * a ≤ c * b
if hc0 : c ≤ 0 then simp [Nat.le_antisymm hc0 (zero_le c), Nat.zero_mul] else
exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_left (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
⊢ c * a ≤ c * b
simp [Nat.le_antisymm hc0 (zero_le c), Nat.zero_mul]
no goals
a b c : Nat
h₁ : a ≤ b
hba : ¬b ≤ a
hc0 : ¬c ≤ 0
⊢ c * a ≤ c * b
exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_left (Nat.not_le.1 hba) (Nat.not_le.1 hc0))