proposition: Lemma Stern_next n: Stern_succ_fct (Stern n) = Stern (n .+1).
proof: Proof. have Ha k: 0 < (fusc k.+1)%:Z by rewrite ltz_nat fusc_gt0. have Hb k: (fusc (k.+1))%:Q != 0 by rewrite intr_eq0 eqz_nat fusc_eq0. rewrite - (odd_double_half n); case: (n./2); case: {n} (odd n)=> // m. rewrite Stern_odd -doubleS Stern_even /Stern /Sba_p /Sba_i. rewrite [X in (1 + X) ^-1] invf_div addf_div1 // addf_div1 // invf_div Sn_gt1 // addrC. move: (f_equal Posz (fusc_normal_rec m.+1)); rewrite - addnn !PoszD - mulz2. by move => <-; rewrite - addrA - mulrBl modz_nat subrr mul0r addr0. rewrite Stern_even Stern_odd /Stern /Sba_i /Sba_p [X in (1 + X) ^-1] invf_div addf_div1 //. rewrite addf_div1 // addrC invf_div Sn_lt1 //. 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)