proposition: Lemma ing_eq : forall x y : F, x [=] y -> inject_Q x [=] inject_Q y.
proof: Proof. intros. unfold inject_Q in |- *. simpl in |- *; intro H0. elim H0; intro. elim a; intros N HN. elim HN; clear H0 a HN; intros e He HN; simpl in HN. apply (less_irreflexive_unfolded _ e). apply leEq_less_trans with ([0]:F); auto. astepr (x[-]x); astepr (y[-]x); eauto with arith. elim b; intros N HN. elim HN; clear H0 b HN; intros e He HN; simpl in HN. apply (less_irreflexive_unfolded _ e). apply leEq_less_trans with ([0]:F); auto. astepr (x[-]x); astepr (x[-]y); eauto with arith. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals