proposition: Lemma Stern_bij_gt0 x: 0 < x -> (0 < Stern_bij x)%N.
proof: Proof. by rewrite /Stern_bij Order.TotalTheory.leNgt => -> /=; rewrite lt0n nat_of_pos_ne0. 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)