proposition: Lemma AbsSmall_cancel_mult : forall e x z : R, [0] [<] z -> AbsSmall (e[*]z) (x[*]z) -> AbsSmall e x.
proof: Proof. unfold AbsSmall in |- *. intros. elim H. intros. split. apply mult_cancel_leEq with (z := z). assumption. rstepl ([--](e[*]z)). assumption. apply mult_cancel_leEq with (z := z). assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2