proposition: Lemma continuant_of0 n: K (nseq n 0) = if odd n then 0 else 1.
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 0) = [:: 0 , 0 & nseq n 0] by []. by rewrite continuantS mul0r add0r Hr //= negbK. 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)