proposition: Lemma CRmult_pos_pos : forall {R : ConstructiveReals} (x y : CRcarrier R), 0 < x * y -> 0 <= x -> 0 <= y -> 0 < x.
proof: Proof. intros. destruct (CRltLinear R). clear p. specialize (s 0 x 1 (CRzero_lt_one R)) as [H2|H2]. - exact H2. - apply CRlt_asym in H2. apply (CRmult_le_compat_r y) in H2. 2: exact H1. rewrite CRmult_1_l in H2. apply (CRlt_le_trans _ _ _ H) in H2. rewrite <- (CRmult_0_l y) in H. apply CRmult_lt_reg_r in H. + exact H. + exact H2. Qed.
imports: QArith Qabs Qround