proposition: Lemma square_pos x : x ≶ 0 → 0 < x * x.
proof: Proof. intros E. apply apart_iff_total_lt in E. destruct E as [E|E]. destruct (decompose_lt E) as [z [Ez1 Ez2]]. apply compose_lt with (z * z). now apply pos_mult_compat. rewrite plus_0_l. apply (left_cancellation (+) (x * z)). rewrite <-plus_mult_distr_r, <-plus_mult_distr_l. rewrite (commutativity z x), <-!Ez2. ring. now apply pos_mult_compat. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.orders MathClasses.orders.maps