proposition: Lemma sternD_odd_rec u v k q n (i:= 2^k * (q.*2.+1)) (S := sternD u v n): i < 2^n -> odd (nth 0 S i) -> odd(nth 0 S i.-1 + nth 0 S i.+1).
proof: Proof. by move => h1 h2; rewrite (sternD_middle_quo _ _ h1) oddM /= odd_double. 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)