proposition: Lemma ing_cancel_less : forall x y : F, inject_Q x [<] inject_Q y -> x [<] y.
proof: Proof. intros x y H. elim H; intros N HN; elim HN; clear H HN; intros e He HN; simpl in HN. apply less_leEq_trans with (x[+]e). apply shift_less_plus'; astepl ([0]:F); auto. apply shift_plus_leEq'; eauto. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals