proposition: Lemma AbsSmall_wdr : rel_wdr R (AbsSmall (R:=R)).
proof: Proof. unfold rel_wdr in |- *. unfold AbsSmall in |- *. intros. elim H; intros. split. astepr y. assumption. astepl y. assumption. Qed.
imports: CoRN.algebra.COrdFields2