I had to prove the following lemma during one of my experiments:
Section Missing. Variable P: nat -> Prop. Lemma asymptotic_because_everywhere: (forall n, P n) -> (\forall n \near \oo, P n). Proof. by exists 0%N. Qed. End Missing.
It must already be there somewhere, but I didn't find under which name... what is it?
Notice that without this lemma, trying
exists 0%N => // in another of my proofs leads to a goal looking like this:
[set n | (0 <= n)%N] `<=` (fun n : nat => P n)
which I found inacceptable: too complex!
With the above lemma, I can solve the same goal with:
apply: asymptotic_because_everywhere. by apply: result_everywhere.
which is nice enough.
Last updated: Feb 05 2023 at 13:02 UTC