proposition: Lemma AbsBig_wdl : Crel_wdl R AbsBig.
proof: Proof. red in |- *. unfold absBig in |- *. intros. elim X. intros H1 H2. split. astepr x. assumption. case H2. intro H3. left. astepl x. assumption. intro H3. right. astepr ([--]x). assumption. Qed.
imports: CoRN.algebra.COrdFields2