proposition: Lemma least_member_glb : forall X a, least_member X a -> forall b, (forall c, In X c -> Le b c) -> Le b a.
proof: Proof. intros X a H b H0; case H;intros H1 H2; apply H0; auto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)