proposition: Lemma SternK: cancel Stern Stern_bij.
proof: Proof. elim/fusc_ind. + by rewrite Stern0 Stern_bij_0. + by rewrite Stern1 Stern_bij_1. + case; first by rewrite Stern0 Stern_bij_0. by move => n Hrec; rewrite Stern_even - {2} Hrec Stern_bij_lt1K // Stern_gt0. + case; first by rewrite Stern1 Stern_bij_1. by move => n Hrec _; rewrite -{2} Hrec Stern_odd Stern_bij_gt1K // Stern_gt0. 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)