proposition: Lemma arith_split_sternD u v n: sternD u v n = add_seq (scale_seq u (rev (stern01 n))) (scale_seq v (stern01 n)).
proof: Proof. rewrite - {1} (addn0 u) - {1} (add0n v) add_sternD. by rewrite - scale_sternD - sternD_rev - scale_sternD !muln0 ! muln1. 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)