proposition: Lemma fib_contentP n (r := fib_content n): fib r.+2 <= n.+1 < fib r.+3.
proof: Proof. rewrite /r /fib_content;case:ex_maxnP => i sa sb; rewrite sa /=. by case: (ltnP (n.+1) (fib i.+3)) => // /sb; rewrite ltnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)