proposition: Lemma CReal_min_lt_r : forall x y : CReal, CReal_min x y < y -> CReal_min x y == x.
proof: Proof. intros. unfold CReal_min. unfold CReal_min in H. 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. } apply (CReal_mult_lt_compat_r 2) in H. 2: apply inject_Q_lt; reflexivity. rewrite CReal_mult_assoc, <- inject_Q_mult in H. setoid_replace ((1 # 2) * 2)%Q with 1%Q in H. 2: reflexivity. rewrite CReal_mult_1_r in H. rewrite CReal_mult_comm, CReal_double in H. intro abs. rewrite CReal_abs_left in H. - unfold CReal_minus in H. rewrite CReal_opp_involutive, CReal_plus_comm in H. rewrite CReal_plus_assoc, <- (CReal_plus_assoc (-x)), CReal_plus_opp_l in H. rewrite CReal_plus_0_l in H. exact (CRealLt_asym _ _ H H). - apply CRealLt_asym, abs. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra