proposition: Lemma fib_content_lt n (r := fib_content n): n.+1 - fib r.+2 < fib r.+1.
proof: Proof. move :(fib_contentP n) => /andP; rewrite -/r; move => [/subnK -{1} <- ]. by rewrite (fibSS r.+1) addnC ltn_add2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)