proposition: Lemma scale_sternD k a b n: sternD (k*a) (k*b) n = scale_seq k (sternD a b n).
proof: Proof. elim: n=> // n /= ->. by elim: (sternD a b n)=> // c [] // d l Ihl /=; rewrite mulnDr -Ihl. 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)