proposition: Lemma fuscq_eq0 n: ((fusc n)%:Q == 0) = (n == 0)%N.
proof: Proof. by rewrite intq_eq0 - (fusc_eq0 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)