proposition: Lemma sternD_nth_compare u v n i (S := (sternD u v n.+1)): i < 2^n -> maxn (nth 0 S (i.*2)) (nth 0 S (i.*2.+2)) <= nth 0 S (i.*2.+1).
proof: Proof. move=> h; have:= (sternD_nth_odd u v h). by rewrite - doubleS ! sternD_nth_even=> ->; rewrite geq_max leq_addr leq_addl. 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)