proposition: Lemma continuant_gt0 l: all (fun z => 0 < z) l -> 0 < K l.
proof: Proof. elim: {l}(size l) {-2}l (leqnn (size l)) => [[] //|n IH]. case => [// | a [| b l]]; first by rewrite /= andbT. rewrite continuantS ltnS -/(size _) => sLn /andP [sa sb]. apply: addr_gt0; first by apply:(mulr_gt0 sa); apply: IH. by apply:(IH _ (ltnW sLn)); move/andP: sb => []. 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)