proposition: Lemma CReal_min_l : forall x y : CReal, CReal_min x y <= x.
proof: Proof. intros. unfold CReal_min. apply (CReal_mult_le_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. rewrite CReal_mult_comm, CReal_double. unfold CReal_minus. rewrite CReal_plus_assoc. apply CReal_plus_le_compat_l. apply (CReal_plus_le_reg_l (CReal_abs (y + - x)+ -x)). ring_simplify. rewrite CReal_plus_comm. apply CReal_le_abs. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra