proposition: Lemma increment_lower_bound_nat : forall (P : nat->Prop) x, lower_bound le P x -> ~ P x -> lower_bound le P (x + 1)%nat.
proof: Proof. Proof using. introv hlo ?. intros y ?. destruct (eq_nat_dec x y). { subst. tauto. } { forwards: hlo; eauto. nat_math. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation LibOrder LibEpsilon) TLC(LibNat)