proposition: Lemma sternD_location_bound b: let H := fun k => exists i, b = nth 0 (stern11 k) i.*2.+1 in 0 < b -> H b.-1 /\ forall k, H k -> k < b.
proof: Proof. move => H bp; split. exists 0 ; rewrite - {1} (prednK bp); elim (b.-1) => // m Ha. by rewrite sternD_nth_odd ?expn_gt0 // - Ha nth0 head_sternD add1n. move => n [k kv]. case: (ltnP (k.*2) (2 ^ n)) => ha. by rewrite kv; exact (sternD_nth_compare_rec (leqnn 1) (leqnn 1) ha). by move: (ltn_eqF bp); rewrite kv nth_default // size_sternD ltnS ha. 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)