fact: Fixpoint sternd_rec s : seq nat := if s is a :: s1 then if s1 is b :: _ then [:: a, a+b & sternd_rec s1] else [:: a] else nil.
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)