proposition: Lemma CRmult_le_reg_r : forall {R : ConstructiveReals} (x y z : CRcarrier R), 0 < x -> y * x <= z * x -> y <= z.
proof: Proof. intros. intro abs. apply (CRmult_lt_compat_r x) in abs. - contradiction. - exact H. Qed.
imports: QArith Qabs Qround