proposition: Lemma CReal_min_max_mult_neg : forall (p q r:CReal), r <= 0 -> CReal_min (r * p) (r * q) == r * CReal_max p q.
proof: Proof. intros p q r H. unfold CReal_min, CReal_max. setoid_replace (r * q - r * p) with (r * (q - p)). 2: ring. rewrite CReal_abs_mult. rewrite (CReal_abs_left r). - ring. - exact H. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra