proposition: Lemma mmin_spec_nat: forall (P:nat->Prop) m, m = mmin le P -> ex P -> P m /\ (forall x, P x -> m <= x).
proof: Proof. Proof using. introv E Q. applys (@mmin_spec _ _ _ P m E Q). applys admits_lower_bound_nat. applys bounded_has_minimal_nat. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation LibOrder LibEpsilon) TLC(LibNat)