proposition: Lemma CRmin_mult : forall {R : ConstructiveReals} (p q r : CRcarrier R), 0 <= r -> CRmin (r * p) (r * q) == r * CRmin p q.
proof: Proof. intros R p q r H. unfold CRmin. setoid_replace (r * q - r * p) with (r * (q - p)). - rewrite CRabs_mult. rewrite (CRabs_right r). 2: exact H. rewrite <- CRmult_assoc. apply CRmult_morph. 2: reflexivity. unfold CRminus. rewrite CRopp_mult_distr_r. do 2 rewrite <- CRmult_plus_distr_l. reflexivity. - unfold CRminus. rewrite CRopp_mult_distr_r. rewrite <- CRmult_plus_distr_l. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms