proposition: Lemma continuant_zeroB l: all (fun z => 0 <= z) l -> K l = 0 -> odd (size l) /\ (forall k, (k.*2 < size l)%N -> nth 0 l k.*2 = 0).
proof: Proof. elim: {l}(size l) {-2}l (leqnn (size l)) => [[] //|n IH]. case => [// | a [ // | b l]]; first by move => _ _ /= az; split => // [] []. rewrite ltnS -/(size _) => /ltnW sa sb sc; case od: odd; last first. by move:(continuant_gt0_odd sb (negbT od)); rewrite sc Order.POrderTheory.ltxx. move: sb; rewrite/all -/(all _ (b::l)) => /andP [sb1 sb2]. move: (sb2)=> /andP [_ sb3]. have ha: 0 <= K l by apply: continuant_ge0. have hb: 0 <= a * K (b :: l) by apply:(mulr_ge0 sb1); apply: continuant_ge0. have : 0 < K (b :: l) by apply:continuant_gt0_odd. rewrite lt0r => /andP [knz _]. move /eqP: sc; rewrite continuantS paddr_eq0 // mulf_eq0 (negbTE knz) orbF. move => /andP [hd /eqP /(IH l sa sb3) [_ kp]]. split => //; case=>[ | k]; first by rewrite (eqP hd). by rewrite doubleS !ltnS => /kp. 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)