proposition: Lemma Stern_numden n: (numq(Stern n) == fusc n) && (denq (Stern n) == fusc n.+1).
proof: Proof. move: (fusc_coprime n). rewrite - {1} (absz_nat (fusc n)) - (absz_nat (fusc n.+1)) => H. rewrite (coprimeq_den H) (coprimeq_num H) eqz_nat sgrEz. by rewrite gtr0_sgz ? gtr0_sgz ? ltz_nat ? lt0n fusc_eq0 //= mul1r // !eqxx. 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)