x : x ≶ 0 -> 0 < x * x. 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). + apply pos_mult_compat;trivial. + rewrite plus_0_l. apply (left_cancellation (+) (x * z)). rewrite <-plus_mult_distr_r, <-plus_mult_distr_l. rewrite (commutativity (f:=plus) z x), <-!Ez2. rewrite mult_0_l,mult_0_r. reflexivity. - apply pos_mult_compat;trivial. Qed.
Require Import