proposition: Lemma stern_ex3 m n: sternD m n 3 = [:: m; 3*m + n; 2*m+n; 3*m+2*n; m+n; 2*m+3*n; m + 2*n; m+3*n ; n].
proof: Proof. simpl. have ->: m + (m + n) = 2* m + n by rewrite addnA addnn mul2n. have ->: m + n + n = m + 2 * n by rewrite - addnA addnn mul2n. rewrite addnA addnACA (addnC _ m) - (mulSn 2 m) addnn - mul2n. by rewrite addnACA addnn - mul2n -addnA (addnC (2*n) n) - (mulSn 2 n). 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)