proposition: Lemma posPartAbsMax : forall x : CReal, CReal_max 0 x == (x + CReal_abs x) * (inject_Q (1#2)).
proof: Proof. split. - intro abs. apply (CReal_mult_lt_compat_r 2) in abs. 2: apply (inject_Q_lt 0 2); reflexivity. rewrite CReal_mult_assoc, <- (inject_Q_mult) in abs. setoid_replace ((1 # 2) * 2)%Q with 1%Q in abs. 2: reflexivity. rewrite CReal_mult_1_r in abs. apply (CReal_plus_lt_compat_l (-x)) in abs. rewrite <- CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_l in abs. apply CReal_abs_le in abs. { exact abs. } split. + rewrite CReal_opp_plus_distr, CReal_opp_involutive. apply (CReal_le_trans _ (x + 0)). 2: rewrite CReal_plus_0_r; apply CRealLe_refl. apply CReal_plus_le_compat_l. apply (CReal_le_trans _ (2 * 0)). * rewrite CReal_opp_mult_distr_l, <- (CReal_mult_comm 2). apply CReal_mult_le_compat_l_half. -- apply inject_Q_lt. reflexivity. -- apply (CReal_plus_le_reg_l (CReal_max 0 x)). rewrite CReal_plus_opp_r, CReal_plus_0_r. apply CReal_max_l. * rewrite CReal_mult_0_r. apply CRealLe_refl. + apply (CReal_plus_le_reg_l x). rewrite <- CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_l. rewrite (inject_Q_plus 1 1), CReal_mult_plus_distr_l, CReal_mult_1_r. apply CReal_plus_le_compat; apply CReal_max_r. - apply CReal_max_lub. + rewrite <- (CReal_mult_0_l (inject_Q (1#2))). do 2 rewrite <- (CReal_mult_comm (inject_Q (1#2))). apply CReal_mult_le_compat_l_half. * apply inject_Q_lt; reflexivity. * rewrite <- (CReal_plus_opp_r x). apply CReal_plus_le_compat_l. rewrite <- CReal_abs_opp. apply CReal_le_abs. + intros abs. apply (CReal_mult_lt_compat_r 2) in abs. 2: apply inject_Q_lt; reflexivity. rewrite CReal_mult_assoc, <- inject_Q_mult in abs. setoid_replace ((1 # 2) * 2)%Q with 1%Q in abs. 2: reflexivity. rewrite CReal_mult_1_r, (inject_Q_plus 1 1), CReal_mult_plus_distr_l, CReal_mult_1_r in abs. apply CReal_plus_lt_reg_l in abs. exact (CReal_le_abs x abs). Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra