proposition: Lemma snumden_inv x: 0 < x -> snumden x = snumden (x^-1).
proof: Proof. rewrite /snumden/snumden' -numq_gt0 -div1r; case/ratP:x => n d. rewrite div1r invf_div addrC coprime_sym =>cp np. rewrite coprimeq_num // coprimeq_den // gtr0_sg // mul1r gtr0_norm //. by move: np; rewrite lt0r => /andP [ /negbTE -> _]. 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)