proposition: Lemma sternD_middle_div u v i n (S := sternD u v n): 0 < i < 2^n -> (nth 0 S i) %| (nth 0 S i.-1 + nth 0 S i.+1).
proof: Proof. move /andP=> [h1]. case:(elogn2P i.-1) => k q; rewrite (prednK h1) => -> sa. by rewrite sternD_middle_quo // -/S /dvdn modnMl. 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)