It takes about 2 minutes for FStar to prove this lemma and what is worse, Emacs becomes intolerably slow as long as it's present. Other, apparently more complicated lemmas do not cause this problem.
let lemma_1 (n: nat) (m: nat) : Lemma (n <= m || n > 0) = ()
Is there an Emacs/FStar option relevant to this matter?
The article at github.com/FStarLang/fstar-mode.el mentions this issue as an Emacs bug. It seems to be present in Emacs 26.3. M-x prettify-symbols-mode resolves it.