proposition: Lemma stern_ex2 m n: sternD m n 2 = [:: m; 2 * m +n; m + n ; m + 2 *n; n].
proof: Proof. by rewrite /= addnA addnn -addnA addnn -!mul2n. 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)