proposition: Lemma CReal_max_lub : forall x y z:CReal, x <= z -> y <= z -> CReal_max x y <= z.
proof: Proof. intros. unfold CReal_max. apply (CReal_mult_le_reg_r 2). - 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. apply (CReal_plus_le_reg_l (-x-y)). ring_simplify. apply CReal_abs_le. split. + unfold CReal_minus. repeat rewrite CReal_opp_plus_distr. do 2 rewrite CReal_opp_involutive. rewrite (CReal_plus_comm x), CReal_plus_assoc. apply CReal_plus_le_compat_l. apply (CReal_plus_le_reg_l (-x)). rewrite <- CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_l. rewrite CReal_mult_comm, CReal_double. rewrite CReal_opp_plus_distr. apply CReal_plus_le_compat; apply CReal_opp_ge_le_contravar; assumption. + unfold CReal_minus. rewrite (CReal_plus_comm y), CReal_plus_assoc. apply CReal_plus_le_compat_l. apply (CReal_plus_le_reg_l y). rewrite <- CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_l. rewrite CReal_mult_comm, CReal_double. apply CReal_plus_le_compat; assumption. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra