proposition: Lemma continuant_cat l a b l' : K (l ++ a::b::l') = K (l ++ [::a]) * K (b::l') + K l * K l'.
proof: Proof. elim: {l}(size l) {-2}l (leqnn (size l))=> [[] //= _ | n IH]. by rewrite mul1r. case=> [/= _|a1 [ _|b1 l]]; first by rewrite mul1r. rewrite !cat1s 2!continuantS; set u := K (b :: l'). by rewrite /= mulrDl mulrDr mulrA mul1r addrAC. rewrite ltnS -/(size _) => sLn. rewrite !cat_cons !continuantS !mulrDl -!mulrA addrACA -mulrDr IH ?(ltnW sLn)//. by rewrite - cat_cons 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)