proposition: Lemma add_sternD a b c d n: sternD (a + c) (b + d) n = add_seq (sternD a b n) (sternD c d n).
proof: Proof. elim: n=> // n /= ->. have: size (sternD a b n) == size (sternD c d n) by rewrite !size_sternD. move: (sternD a b n)(sternD c d n); apply: seq2_ind => // e f []; first by case. move=> g l1 [] // h l2. by rewrite /= -/(sternd_rec (h::l2)) -/(sternd_rec (g::l1)) addnACA => ->. 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)