proposition: Lemma CRmult_pos_appart_zero : forall {R : ConstructiveReals} (x y : CRcarrier R), 0 < x * y -> 0 ≶ x.
proof: Proof. intros. destruct (CRltLinear R). clear p. pose proof (s 0 x 1 (CRzero_lt_one R)) as [H0|H0]. { left. exact H0. } destruct (s 0 y (x*y) H). - left. rewrite <- (CRmult_0_l y) in H. apply CRmult_lt_reg_r in H. + exact H. + exact c. - right. apply CRopp_lt_cancel. rewrite CRopp_0. apply (CRmult_pos_pos (-x) (-y)). + rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r, CRopp_involutive. exact H. + rewrite <- CRopp_0. apply CRopp_ge_le_contravar. intro abs. rewrite <- (CRmult_0_r x) in H. apply CRmult_lt_reg_l in H. * rewrite <- (CRmult_1_l y) in c. rewrite <- CRmult_assoc in c. apply CRmult_lt_reg_r in c. -- rewrite CRmult_1_r in c. exact (CRlt_asym _ _ H0 c). -- exact H. * exact abs. + intro abs. apply (CRmult_lt_compat_r y) in H0. * rewrite CRmult_1_l in H0. exact (CRlt_asym _ _ H0 c). * apply CRopp_lt_cancel. rewrite CRopp_0. exact abs. Qed.
imports: QArith Qabs Qround