proposition: Lemma ing_ap : forall x y : F, x [#] y -> inject_Q x [#] inject_Q y.
proof: Proof. intros x y H; elim (ap_imp_less _ _ _ H); intro Hlt; [ left | right ]; apply ing_lt; auto. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals