proposition: Lemma SubON_successor : forall a b, Successor a b <-> Successor (f a) (f b).
proof: Proof. split; intro H. - destruct H. split. + now apply SubON_mono. + intros z Hz Hz'; destruct (SubON_onto z). * transitivity (f a); auto. apply SubON_incl. * subst; apply SubON_mono in Hz; apply SubON_mono in Hz'. eapply H0;eauto. - destruct H; split. + now apply SubON_mono. + intros z Hz Hz'; specialize (H0 (f z)). apply H0; now apply SubON_mono. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles) hydras(OrdNotations Schutte_basics)