Library ZFord_equiv

Require ZFord ZFordcl.
Import ZFnats.
Import IZF.

Lemma isOrd_eqv1 : forall x,
  ZFord.isOrd x -> ZFordcl.isOrd x.

Lemma isOrd_equiv : forall x,
  ZFord.isOrd x <-> ZFordcl.isOrd x.

Lemma succ_equiv : forall x,
  ZFord.isOrd x -> succ x == ZFord.osucc x.

Hint Resolve isOrd_eqv1.