proposition: Lemma continuant_zeroA l: odd (size l) -> (forall k, (k.*2 < size l)%N -> nth 0 l k.*2 = 0) -> K l = 0.
proof: Proof. elim: {l}(size l) {-2}l (leqnn (size l)) => [[] //|n IH]. case => [// | a [ // | b l]]; first by move => _ _ ep /=; apply: (ep 0%N). rewrite /size /odd negbK -/(size _) - /(odd _) => /ltnW sa sb sc. have az: a = 0 by apply: (sc 0%N). rewrite continuantS az mul0r add0r; apply: IH => // k kl. by move: (sc k.+1); rewrite doubleS !ltnS /=; apply. 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)