proposition: Lemma Stern_bij_lt1 x : 0 < x < 1 -> Stern_bij x = (Stern_bij (Sba_j x)).*2.
proof: Proof. move => h. move/andP: (h) => [xp _]. move: (Stern_bij1_lt1 h). rewrite /Stern_bij ! Order.TotalTheory.leNgt (Sba_j_pos h) xp /negb => -> /=. by rewrite 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)