proposition: Lemma continuant_rcons a b l : K (rcons (rcons l b) a) = a * K (rcons l b) + K l.
proof: Proof. by move: (continuant_cat l b a nil); rewrite /= mulr1 mulrC -cat_rcons !cats1. 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)