proposition: Fact fib_cont_aux2 n i: fib i.+2 <= n.+1 -> i <= n.
proof: Proof. by move /(leq_trans (fib_gen i.+1)); rewrite ltnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)