proposition: Lemma fusc_coprime n: coprime (fusc n) (fusc n.+1).
proof: Proof. elim /fusc_ind:n; [ done | done | move => n H | move => n H _]. by rewrite fusc_even fusc_odd /coprime gcdnDl. by rewrite - doubleS fusc_even fusc_odd /coprime gcdnC gcdnDr gcdnC. 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)