proposition: Lemma split_sternD_right u v n : drop (2^n) (sternD u v n.+1) = sternD (u + v) v n.
proof: Proof. rewrite split_sternD sternD_split2 {2} (sternD_split1 (u+v)) cat_rcons. by rewrite drop_size_cat // size_belast size_behead size_sternD. 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)