proposition: Lemma Rsqr_pos_lt : forall x:R, x <> 0 -> 0 < Rsqr x.
proof: Proof. intros; case (Rtotal_order 0 x); intro; [ unfold Rsqr; apply Rmult_lt_0_compat; assumption | elim H0; intro; [ elim H; symmetry ; exact H1 | rewrite Rsqr_neg; generalize (Ropp_lt_gt_contravar x 0 H1); rewrite Ropp_0; intro; unfold Rsqr; apply Rmult_lt_0_compat; assumption ] ]. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun