proposition: Lemma sternD_ge_in_bounds u v n i: 0 < i < 2^n -> u + v <= nth 0 (sternD u v n) i.
proof: Proof. move => /andP[ka kb]; rewrite (sternD_stern _ _ (ltnW kb)). by apply: leq_add; apply:leq_pmulr; rewrite stern_gt0 // subn_gt0. 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)