no goals
d✝ : ℤ
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (x * z) * (c * (x * z)) ≤ d * (y * w) * (d * (y * w))
simpa [mul_comm, mul_left_comm] using mul_le_mul xy zw (Nat.zero_le _) (Nat.zero_le _)