proposition: Lemma AbsBig_wdr : Crel_wdr R AbsBig.
proof: Proof. red in |- *. intros. unfold absBig in |- *. unfold absBig in H. elim X. intros H1 H2. split. assumption. case H2. intro H3. left. apply leEq_wdr with y. assumption. assumption. intro H3. right. apply leEq_wdl with y. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2