proposition: Lemma continuant_rev l : K (rev l) = K l.
proof: Proof. elim: {l}(size l) {-2}l (leqnn (size l)) => [[] //|n IH]. case => [// | a [// | b l]]; rewrite ltnS -/(size _) => sLn. by rewrite !rev_cons continuant_rcons -rev_cons !IH //= ltnW. 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)