proposition: Lemma continuant_fib n : K (nseq n 1) = (fib n.+1)%:Z%:Q.
proof: Proof. elim: n {-2} (n) (leqnSn n) => [ [// | [] //] | n Hr m]. rewrite (leq_eqVlt) ltnS; case/orP; [move => /eqP -> | by apply: Hr]. have ->: (nseq n.+2 1) = [:: 1 , 1 & nseq n 1] by []. rewrite continuantS Hr // mul1r -[(1 :: nseq n 1)]/(nseq n.+1 1) Hr //. by rewrite - ratN_D - fibSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)