proposition: Lemma Stern_bij1_inj x y: 0 < x -> 0 < y -> Stern_bij1 x = Stern_bij1 y -> x = y.
proof: Proof. move: (leq_maxl (snumden x) (snumden y)) (leq_maxr (snumden x) (snumden y)). move: (maxn _ _) => k; elim: k x y => [ x y | n Hrec x y]. by rewrite leqn0 => sa _ /snumden_gt0; rewrite sa. wlog lexy: x y / x <= y. move => H l1 l2 xp yp eq; case /orP: (Order.TotalTheory.le_total x y) => l3;first by apply:H. by symmetry; apply: H. move => lxn lyn xp yp. case:(ltrgtP 1 x) => cx1. + have l1y := (Order.POrderTheory.lt_le_trans cx1 lexy). rewrite (Stern_bij1_gt1 cx1) (Stern_bij1_gt1 l1y); case => eq'. rewrite - (Sba_mK x) - (Sba_mK y). move:(Sba_m_pos cx1) (Sba_m_pos l1y) => xp' yp'. move: (leq_trans (Sba_m_snum cx1) lxn) (leq_trans(Sba_m_snum l1y) lyn). by rewrite !ltnS => lxn' lyn'; rewrite (Hrec _ _ lxn' lyn' xp' yp' eq'). + have lx1 : 0 < x < 1 by rewrite xp cx1. case :(ltrgtP 1 y) => cy1. * by rewrite (Stern_bij1_gt1 cy1) (Stern_bij1_lt1 lx1). * have ly1 : 0 < y < 1 by rewrite yp cy1. rewrite (Stern_bij1_lt1 ly1) (Stern_bij1_lt1 lx1); case => eq'. rewrite -(Sba_jK x) -(Sba_jK y). move:(Sba_j_pos lx1) (Sba_j_pos ly1) => xp' yp'. move: (leq_trans (Sba_j_snum lx1) lxn) (leq_trans(Sba_j_snum ly1) lyn). by rewrite !ltnS => lxn' lyn'; rewrite (Hrec _ _ lxn' lyn' xp' yp' eq'). * by rewrite - cy1 Stern_bij1_1 (Stern_bij1_lt1 lx1). + rewrite - cx1; case y1: (y==1); first by rewrite (eqP y1). have l1y: 1 < y by rewrite Order.POrderTheory.lt_neqAle; rewrite eq_sym y1 cx1. by rewrite Stern_bij1_1 (Stern_bij1_gt1 l1y). 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)