proposition: Lemma div_resp_AbsSmall: forall (R: COrdField) (x y e : R) (H: [0][<]y), AbsSmall e x -> AbsSmall (e[/]y[//]pos_ap_zero _ _ H) (x[/]y[//]pos_ap_zero _ _ H).
proof: Proof. unfold AbsSmall. intros. destruct H0. split. rstepl (([--]e)[/]y[//]pos_ap_zero _ _ H). apply div_resp_leEq; auto. apply div_resp_leEq; auto. Qed.
imports: CoRN.algebra.COrdFields2