proposition: Lemma inv0 : inv 0%:F = 0%:F.
proof: Proof. rewrite !piE /invf !numden_Ratio ?oner_eq0 // /Ratio /insubd. do 2?case: insubP; rewrite //= ?eqxx ?oner_eq0 // => u _ hu _. by congr \pi; apply: val_inj; rewrite /= hu. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)