proposition: Theorem least_member_unicity : forall X a b, least_member X a -> least_member X b -> a = b.
proof: Proof. intros X a b H H0; case H;case H0;intros. - apply Le_antisym;auto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)