proposition: Lemma sternD_bound2 n i: i <= 2 ^ n -> nth 0 (stern11 n.+1) i <= (nth 0 (stern11 n) i).*2 ?= iff (i==2^n).
proof: Proof. move => ha. rewrite (sternD_col_progression ha) - addnn. set f := addn (nth 0 (stern11 n) i). have hb: {mono f : m n / m <= n} by move => u v /=; rewrite /f leq_add2l. by rewrite (mono_leqif hb) //; apply: sternD_bound1. 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)