proposition: Lemma fib_content_eq n: fib_content ((fib n.+2).-1) = n.
proof: Proof. move: (fib_contentP (fib n.+2).-1). rewrite /= - fib_pos => /andP[sa /fib_monotone_bis]. rewrite !ltnS leq_eqVlt; case/orP; first by move/eqP. by move => /fib_smonotone_bis; rewrite ltnNge sa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)