proposition: Lemma SubON_least : forall a , Least a <-> Least (f a).
proof: Proof. split; intro H. - intros y; destruct (comparable_comp_spec (f a) y). + subst y; right. + now left. + exfalso. { destruct (SubON_onto y). transitivity (f a); auto. apply SubON_incl. subst y; apply SubON_mono in H0. destruct (H x). apply (StrictOrder_Irreflexive a). now transitivity y. apply (StrictOrder_Irreflexive a). auto. } - intro x; destruct (comparable_comp_spec a x). subst; right. + now left. + apply SubON_mono in H0; specialize (H (f x)). exfalso. { apply (StrictOrder_Irreflexive (f a)). destruct H. transitivity y; auto. auto. } Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles) hydras(OrdNotations Schutte_basics)