proposition: Lemma SB_to_rat_val n: SB_to_rat (pos_of_nat' n) = Stern (n.+1).
proof: Proof. rewrite - (bin_of_natK n.+1) /pos_of_nat' => /=. elim: (pos_of_nat n n) => // p /= ->; rewrite natTrecE - ?Stern_odd //. move:(nat_of_pos_ne0 p); case: (nat_of_pos p) => // q _. symmetry; apply:Stern_even. 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)