proposition: Lemma least_member_lower_bound : forall X a, least_member X a -> forall b, In X b -> Le a b.
proof: Proof. intros X a H; case H. unfold In; intuition. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)