proposition: Theorem least_member_of_eq : forall (X Y : Ensemble M) a b , Included X Y -> Included Y X -> least_member X a -> least_member Y b -> a = b.
proof: Proof. intros X Y a b H H0 [H3 H4 ] [H6 H7]. apply Le_antisym;auto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)