proposition: Lemma sternD_middle u v n : nth 0 (sternD u v n.+1) (2^n) = u + v.
proof: Proof. rewrite split_sternD nth_cat size_sternD /= ltnS leqnn. exact: (proj2 (sternD_at_bounds u (u + v) n)). 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)