proposition: Lemma Stern_injective: injective Stern.
proof: Proof. move => n m eq1. move: (Stern_numden n) (Stern_numden m) => /andP [/eqP e1 /eqP e2] /andP[e3 e4]. by apply: fusc2_injective; apply /eqP; rewrite - eqz_nat -?e1 - ?e2 eq1. 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)