proposition: Lemma Stern_bij_gt1 x : 1 < x -> Stern_bij x = (Stern_bij (Sba_m x)).*2.+1.
proof: Proof. move => h. move:(Stern_bij1_gt1 h);rewrite /Stern_bij ! Order.TotalTheory.leNgt (Stern_bij1_gt1 h). by rewrite (Sba_m_pos h) (Order.POrderTheory.lt_trans ltr01 h) /= natTrecE. 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)