proposition: Lemma square_nonneg x : 0 ≤ x * x.
proof: Proof. apply not_lt_le_flip. intros E. destruct (lt_antisym (x * x) 0). split; [easy |]. apply square_pos. apply (strong_extensionality (x *.)). rewrite mult_0_r. now apply lt_apart. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.orders MathClasses.orders.maps