proposition: Lemma Stern_bij_inj x y: 0 <= x -> 0 <= y -> Stern_bij x = Stern_bij y -> x = y.
proof: Proof. have H w: (0 < w) ==> (Stern_bij w != 0)%N. by rewrite - lt0n; apply/implyP/Stern_bij_gt0. move => sa sb sc;move:sa sb sc (H x)(H y). rewrite /Stern_bij; case: (ltrgt0P x) => //; case: (ltrgt0P y) => //. + by move => xp yp _ _ / nat_of_pos_inj/Stern_bij1_inj h _ _; apply h. + by move => _ _ _ _ ->. + by move => _ _ _ _ <-. + by move => -> ->. 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)