proposition: Lemma fusc_pair_surj a b: coprime a b.+1 -> {n | a = fusc n /\ b.+1 = fusc n.+1 }.
proof: Proof. rewrite - {1} (absz_nat a) - (absz_nat (b.+1)) => H. set x := (a)%:Q / (b.+1)%:Q. have: 0 <= x by apply:divr_ge0; rewrite ler0n. move /Stern_surjective => [n eqx]; move: (Stern_numden n). rewrite - eqx /x (coprimeq_den H)(coprimeq_num H) sgrEz gtr0_sgz // mul1r. by rewrite !eqz_nat //=;move/andP => [/eqP -> /eqP ->]; exists n. 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)