proposition: Lemma AbsBig_wdr_unfolded : forall x y z : R, AbsBig x y -> y [=] z -> AbsBig x z.
proof: Proof. Proof AbsBig_wdr. Lemma AbsBig_wdl_unfolded : forall x y z : R, AbsBig x y -> x [=] z -> AbsBig z y. Proof AbsBig_wdl. End absBig_wd_properties. Declare Left Step AbsBig_wdl_unfolded. Declare Right Step AbsBig_wdr_unfolded. Add Parametric Morphism c : (@AbsSmall c) with signature (@cs_eq (cof_crr c)) ==> (@cs_eq c) ==> iff as AbsSmall_morph_wd. Proof with try assumption. intros x1 x2 xeq y1 y2 yeq. split; intro H. stepr y1... stepl x1... symmetry in xeq, yeq. stepr y2... stepl x2... Qed.
imports: CoRN.algebra.COrdFields2