proposition: Lemma ing_cancel_AbsSmall : forall e x y : F, AbsSmall (inject_Q e) (inject_Q x[-]inject_Q y) -> AbsSmall e (x[-]y).
proof: Proof. intros. elim H. intros H0 H1. split. apply ing_cancel_leEq. astepl ( [--] (inject_Q e)). astepr (inject_Q x[-]inject_Q y). assumption. astepl (inject_Q x[+][--] (inject_Q y)). apply eq_transitive_unfolded with (inject_Q x[+]inject_Q [--]y). apply plus_resp_eq. apply eq_symmetric_unfolded. apply ing_min. Step_final (inject_Q (x[+][--]y)). apply eq_symmetric_unfolded. apply ing_plus. apply eq_symmetric_unfolded. apply ing_min. apply ing_cancel_leEq. astepl (inject_Q x[-]inject_Q y). assumption. astepl (inject_Q x[+][--] (inject_Q y)). apply eq_transitive_unfolded with (inject_Q x[+]inject_Q [--]y). apply plus_resp_eq. apply eq_symmetric_unfolded. apply ing_min. Step_final (inject_Q (x[+][--]y)). apply eq_symmetric_unfolded. apply ing_plus. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals