proposition: Lemma Stern_surjective x: 0 <= x -> {n | x = Stern n}.
proof: Proof. move => h; exists (Stern_bij x); move:h. rewrite le0r; case/orP;first by move/eqP ->;rewrite Stern_bij_0 Stern0. move: (leqnn (snumden x)); rewrite - ltnS; move:{2} (_ .+1) => k. elim :k x => // n Hx x le1 xp. have Hb z: (z < snumden x -> z < n)%N by move => h; exact: (leq_trans h le1). case :(ltrgtP x 1) => lx1. have ll: 0 < x < 1 by rewrite xp lx1. have pa:=(Sba_j_pos ll). rewrite (Stern_bij_lt1 ll) - {1} (Sba_jK x). move: (Hx _ (Hb _ (Sba_j_snum ll)) pa). by rewrite - (prednK(Stern_bij_gt0 pa)) Stern_even => <-. + rewrite (Stern_bij_gt1 lx1) Stern_odd. by rewrite - (Hx _ (Hb _ (Sba_m_snum lx1)) (Sba_m_pos lx1)) Sba_mK. + by rewrite lx1 Stern_bij_1 Stern1. 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)