proposition: Lemma sternD_bound1 i n: i <= 2 ^n -> stern i <= (nth 0 (stern11 n) i) ?= iff (i == 2 ^ n).
proof: Proof. move => ha; rewrite nth_stern11_alt //. apply/leqifP; case hb: (i == 2 ^ n);first by rewrite (eqP hb) subnn add0n eqxx. by apply/ltn_paddl; rewrite stern_gt0 subn_gt0 ltn_neqAle ha hb. 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)