proposition: Lemma Stern_bij1_surj p: { x | (0 < x) /\ (Stern_bij1 x = p) }.
proof: Proof. elim: p => [ p [x [xp ev]] | p [x [xp ev]] | ]. + move: (Order.POrderTheory.lt_trans ltr01 (Sba_p_pos xp)) => lt2. by exists (Sba_p x); rewrite Stern_bij1_gt1K // ev. + move: (Sba_i_pos xp) => /andP [lt1 _]. by exists (Sba_i x); rewrite Stern_bij1_lt1K // ev. by exists 1. 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)