proposition: Lemma AbsBigSmall_minus : forall (R : COrdField) (e1 e2 x1 x2 : R), e2 [<] e1 -> AbsBig e1 x1 -> AbsSmall e2 x2 -> AbsBig (e1[-]e2) (x1[-]x2).
proof: Proof. intros. unfold absBig in |- *. split. apply plus_cancel_less with (z := e2). rstepl e2. rstepr e1. assumption. unfold absBig in X0. elim X0. intros H2 H3. case H3. intro H4. left. unfold AbsSmall in H. elim H. intros. rstepl (e1[+][--]e2). rstepr (x1[+][--]x2). apply plus_resp_leEq_both. assumption. apply inv_cancel_leEq. rstepl x2. rstepr e2. assumption. intro H4. right. unfold AbsSmall in H. elim H. intros H5 H6. rstepr ([--]e1[+]e2). rstepl (x1[+][--]x2). apply plus_resp_leEq_both. assumption. apply inv_cancel_leEq. rstepr x2. rstepl ([--]e2). assumption. Qed.
imports: CoRN.algebra.COrdFields2