proposition: Lemma Stern_bij1_gt1 x : 1 < x -> Stern_bij1 x = xI (Stern_bij1 (Sba_m x)).
proof: Proof. move => xp1; rewrite - (Stern_bij_recE (Sba_m_pos xp1) (Sba_m_snum xp1)). by rewrite {1} /Stern_bij1 /= (Order.TotalTheory.ltNge x 1) (Order.POrderTheory.ltW xp1) andbF xp1. 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)