proposition: Lemma ing_le : forall x y : F, x [<=] y -> inject_Q x [<=] inject_Q y.
proof: Proof. intros. intro. rewrite -> leEq_def in H; apply H. apply ing_cancel_less. auto. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals