proposition: Lemma Stern_consecutive_rec a r n: Stern_consecutive a r -> Stern_consecutive a (n *a + r).
proof: Proof. elim: n => // n H /H [m [i [pa pb pc]]];rewrite mulSn - addnA. exists (m.+1), i.*2. by rewrite sternD_nth_even sternD_nth_odd ? pa // pb pc expn2S ltn_double. 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)