proposition: Lemma bounded_has_minimal_nat : @bounded_has_minimal nat le.
proof: Proof. Proof using. intros P [ y ? ]. cut ( forall (k x : nat), (y + 1 - x)%nat = k -> lower_bound le P x -> exists z, min_element le P z ). { intros ? [ x ? ]. eauto. } induction k; introv ? hlo. { false. forwards: hlo; eauto. nat_math. } destruct (prop_inv (P x)). { exists x. split; eauto. } { eapply (IHk (x + 1)%nat). nat_math. eauto using increment_lower_bound_nat. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation LibOrder LibEpsilon) TLC(LibNat)