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