proposition: Lemma dec_inh_nat_subset_has_unique_least_element : forall P:nat->Prop, (forall n, P n \/ ~ P n) -> (exists n, P n) -> has_unique_least_element le P.
proof: Proof. intros P Pdec (n0,HPn0). assert (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') \/ (forall n', P n' -> n<=n')) as H. { intro n; induction n as [|n IHn]. - right. intros. apply Nat.le_0_l. - destruct IHn as [(n' & IH1 & IH2)|IH]. + left. exists n'; auto. + destruct (Pdec n) as [HP|HP]. * left. exists n; auto. * right. intros n' Hn'. apply Nat.le_neq; split; auto. intros <-. auto. } destruct (H n0) as [(n & H1 & H2 & H3)|H0]; [exists n | exists n0]; repeat split; trivial; intros n' (HPn',Hn'); apply Nat.le_antisymm; auto. Qed.
imports: PeanoNat Compare_dec Decidable