fact: Definition Stern_consecutive a b:= exists n i, [/\ i < 2^n, nth 0 (stern11 n) i = a & nth 0 (stern11 n) i.+1 = b].
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)