proposition: Lemma Stern_even n: Stern ((n.+1).*2) = Sba_i (Stern (n.+1)).
proof: Proof. rewrite /Stern /Sba_i fusc_even fusc_odd ratN_D [X in 1 + X] invf_div. rewrite addrC addf_div1; first by rewrite [in RHS] invf_div. by rewrite pnatr_eq0 fusc_eq0. 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)