proposition: Lemma CReal_min_lt : forall x y z : CReal, z < x -> z < y -> z < CReal_min x y.
proof: Proof. intros. unfold CReal_min. apply (CReal_mult_lt_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_lt_reg_l (CReal_abs (y - x) - (z*2))). ring_simplify. apply Rabs_def1. - unfold CReal_minus. rewrite <- (CReal_plus_comm y). apply CReal_plus_lt_compat_l. apply (CReal_plus_lt_reg_r (-x)). rewrite CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_r. rewrite <- CReal_double, CReal_mult_comm. apply CReal_mult_lt_compat_r. + apply inject_Q_lt; reflexivity. + apply CReal_opp_gt_lt_contravar, H. - unfold CReal_minus. rewrite CReal_opp_plus_distr, CReal_opp_involutive. rewrite CReal_plus_comm, (CReal_plus_comm (-z*2)), CReal_plus_assoc. apply CReal_plus_lt_compat_l. apply (CReal_plus_lt_reg_r (-y)). rewrite CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_r. rewrite <- CReal_double, CReal_mult_comm. apply CReal_mult_lt_compat_r. + apply inject_Q_lt; reflexivity. + apply CReal_opp_gt_lt_contravar, H0. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra