proposition: Lemma AbsSmall_eps_div_two : forall e x1 x2 : R, AbsSmall (e [/]TwoNZ) x1 -> AbsSmall (e [/]TwoNZ) x2 -> AbsSmall e (x1[+]x2).
proof: Proof. intros. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2