proposition: Lemma ing_cancel_eq : forall x y : F, inject_Q x [=] inject_Q y -> x [=] y.
proof: Proof. intros x y Hxy. apply not_ap_imp_eq; intro Hap. elim (ap_irreflexive_unfolded _ (inject_Q x)). astepr (inject_Q y). apply ing_ap; auto. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals