proposition: Lemma negPartAbsMin : forall x : CReal, CReal_min 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_r (CReal_abs x)) in abs. unfold CReal_minus in abs. rewrite CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r in abs. apply (CReal_plus_lt_compat_l (-(CReal_min 0 x * 2))) in abs. rewrite <- CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_l in abs. apply CReal_abs_lt in abs. destruct abs. apply (CReal_plus_lt_compat_l (CReal_min 0 x * 2)) in c0. rewrite <- CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_l in c0. apply (CReal_plus_lt_compat_r x) in c0. rewrite CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r in c0. rewrite <- CReal_double, CReal_mult_comm in c0. apply CReal_mult_lt_reg_l in c0. + apply CReal_min_lt_r in c0. rewrite c0, CReal_mult_0_l, CReal_opp_0, CReal_plus_0_l in c. exact (CRealLt_asym _ _ c c). + apply inject_Q_lt; reflexivity. - intro abs. assert ((x - CReal_abs x) * inject_Q (1 # 2) < 0 * inject_Q (1 # 2)). { rewrite CReal_mult_0_l. apply (CReal_lt_le_trans _ _ _ abs). apply CReal_min_l. } apply CReal_mult_lt_reg_r in H. 2: apply inject_Q_lt; reflexivity. rewrite <- (CReal_plus_opp_r (CReal_abs x)) in H. apply CReal_plus_lt_reg_r, CReal_abs_gt in H. rewrite CReal_min_right, <- CReal_abs_opp, CReal_abs_right in abs. + unfold CReal_minus in abs. rewrite CReal_opp_involutive, <- CReal_double, CReal_mult_comm in abs. rewrite <- CReal_mult_assoc, <- inject_Q_mult in abs. setoid_replace ((1 # 2) * 2)%Q with 1%Q in abs. * rewrite CReal_mult_1_l in abs. exact (CRealLt_asym _ _ abs abs). * reflexivity. + rewrite <- CReal_opp_0. apply CReal_opp_ge_le_contravar, CRealLt_asym, H. + apply CRealLt_asym, H. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra