proposition: Lemma Stern_bij_recE (x:rat) n : 0 < x -> ((snumden x) < n)%N -> Stern_bij_rec x n = Stern_bij1 x.
proof: Proof. elim: n {-2} n (leqnn n) x => [[] | n Hr k] //. rewrite leq_eqVlt ltnS; case /orP; last by move => le; apply: Hr. move /eqP -> => x xp; rewrite ltnS => le2. have Hb z: (z < snumden x -> z < n)%N by move => h; exact: (leq_trans h le2). case: (ltrgtP x 1) => lx1. + have ll: 0 < x < 1 by rewrite xp lx1. move:(Sba_j_pos ll) (Sba_j_snum ll) => sa sb; move:(Hb _ sb) => sc. by rewrite /= ll Hr // {2} /Stern_bij1 /= ll Hr. + have ll: (0 < x < 1) = false by rewrite xp Order.TotalTheory.ltNge (Order.POrderTheory.ltW lx1). move:(Sba_m_pos lx1) (Sba_m_snum lx1) => sa sb; move:(Hb _ sb) => sc. by rewrite /= ll lx1 Hr // {2} /Stern_bij1 /= ll lx1 Hr. + by rewrite lx1. 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)