proposition: Lemma AbsSmall_wdr_unfolded : forall x y z : R, AbsSmall x y -> y [=] z -> AbsSmall x z.
proof: Proof. Proof AbsSmall_wdr. Lemma AbsSmall_wdl : rel_wdl R (AbsSmall (R:=R)). Proof. unfold rel_wdl in |- *. unfold AbsSmall in |- *. intros. elim H; intros. split. astepl ([--]x). assumption. astepr x. assumption. Qed.
imports: CoRN.algebra.COrdFields2