proposition: Lemma CReal_max_right : forall x y : CReal, x <= y -> CReal_max x y == y.
proof: Proof. intros. unfold CReal_max. apply (CReal_mult_eq_reg_r 2). 2: right; apply inject_Q_lt; reflexivity. rewrite CReal_mult_assoc, <- inject_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite CReal_mult_1_r. rewrite CReal_mult_comm, CReal_double. rewrite CReal_abs_right. - ring. - rewrite <- (CReal_plus_opp_r x). apply CReal_plus_le_compat. + exact H. + apply CRealLe_refl. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra