proposition: Lemma CReal_min_plus : forall (x y z : CReal), x + CReal_min y z == CReal_min (x + y) (x + z).
proof: Proof. intros. unfold CReal_min. setoid_replace (x + z - (x + y)) with (z-y). 2: ring. apply (CReal_mult_eq_reg_r 2). 2: right; apply inject_Q_lt; reflexivity. rewrite CReal_mult_plus_distr_r. 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_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. ring. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra