proposition: Lemma AbsSmall_plus : forall e1 e2 x1 x2 : R, AbsSmall e1 x1 -> AbsSmall e2 x2 -> AbsSmall (e1[+]e2) (x1[+]x2).
proof: Proof. unfold AbsSmall in |- *. intros. elim H; intros. elim H0; intros. split. rstepl ([--]e1[+][--]e2). apply plus_resp_leEq_both; assumption. apply plus_resp_leEq_both; assumption. Qed.
imports: CoRN.algebra.COrdFields2