proposition: Lemma sternD_positive u v n i : 0 < u -> 0 < v -> i <= 2^n -> 0 < nth 0 (sternD u v n) i.
proof: Proof. move: (sternD_at_bounds u v n) => [sa sb] ap bp kn. case l2: (0 < i < 2^n). apply: (leq_trans _ (sternD_ge_in_bounds u v l2)). by rewrite (addn_gt0 u v) ap bp. move: (negbT l2); rewrite negb_and - leqNgt leqn0 ltn_neqAle kn andbT /= negbK. by case /orP; move/ eqP ->; rewrite ? sa ?sb. 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)