fact: Fixpoint continuant (l : seq rat) := if l is a :: l1 then if l1 is b :: l2 then a * (continuant l1) + continuant l2 else a else 1.
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)