proposition: Lemma sternd_rec_aux a s: s != nil -> sternd_rec (a::s) = [:: a, (a + head 0 s) & sternd_rec s].
proof: Proof. by case: s. 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)