proposition: Lemma continuant_gt0_odd l: all (fun z => 0 <= z) l -> ~~odd (size l) -> 0 < K l.
proof: Proof. elim: {l}(size l) {-2}l (leqnn (size l)) => [[] //|n IH]. case => [// | a [ // | b l]]. rewrite continuantS ltnS -/(size _) => /ltnW sLn /andP [sa sb]. move/andP: (sb); rewrite [odd _]/= negbK => [][_ sc] os. have: 0 <= a * K (b :: l) by apply: (mulr_ge0 sa); apply:continuant_ge0. by rewrite - (lerDr (K l));apply: Order.POrderTheory.lt_le_trans; apply:IH. 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)