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