proposition: Lemma admits_lower_bound_nat : forall (P : nat->Prop), ex (lower_bound le P).
proof: Proof. Proof using. exists 0%nat. unfold lower_bound. nat_math. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation LibOrder LibEpsilon) TLC(LibNat)