proposition: Lemma sternD_stern u v n i: i <= 2^n -> nth 0 (sternD u v n) i = u * (stern (2^n - i)) + v * (stern i).
proof: Proof. move => sa. rewrite arith_split_sternD. have kl1: i < (2 ^ n).+1 by rewrite ltnS. set l1 := scale_seq _ _; set l2 := scale_seq _ _. have sl1: size l1 = (2^n).+1. by rewrite /l1 - sternD_rev - scale_sternD size_sternD. have sl2: size l2 = (2^n).+1 by rewrite /l2 - scale_sternD size_sternD. have sl1l2: size l1 = size l2 by rewrite sl1 sl2. have k1: i < size (stern01 n) by rewrite size_sternD. have k2: i < size (rev (stern01 n)) by rewrite - sternD_rev size_sternD. have kz: i < size (zip l1 l2) by rewrite size_zip sl1 sl2 minnn. rewrite /add_seq (nth_map (0,0) _ _ kz) // nth_zip //=. rewrite /l1 /scale_seq (nth_map 0 _ _ k2) /l2 /scale_seq (nth_map 0 _ _ k1). rewrite (nth_rev _ k1) {2} /stern01 size_sternD subSS. by rewrite stern_prop ?leq_subr // (stern_prop sa). 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)