proposition: Lemma SubON_limit : forall a , Limit a <-> Limit (f a).
proof: Proof. split; intro H. - destruct H ; split. + destruct H as [m Hm]; exists (f m); now apply SubON_mono. + intros y Hy; destruct (SubON_onto y) as [x Hx]. * transitivity (f a); auto. apply SubON_incl. * subst; apply SubON_mono in Hy. destruct (H0 _ Hy) as [z [Hz Hz']]. exists (f z); split; apply SubON_mono; auto. - destruct H; split. + destruct H as [w Hw]; destruct (SubON_onto w) as [x Hx]. transitivity (f a); auto. * apply SubON_incl. * exists x; subst w; apply SubON_mono in Hw; auto. + intros y Hy; destruct (H0 (f y)) as [w [Hw Hw']]. * apply SubON_mono; auto. * destruct (SubON_onto w) as [x Hx]. transitivity (f a); auto; apply SubON_incl. subst w; exists x; split;apply SubON_mono; auto. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles) hydras(OrdNotations Schutte_basics)