proposition: Lemma Stern_bijK x: 0 <= x -> x = Stern (Stern_bij x).
proof: Proof. move => h. by move: (Stern_bij_inj (Stern_ge0 (Stern_bij x)) h (SternK (Stern_bij x))). 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)