proposition: Lemma ereprK : cancel erepr pi.
proof: Proof. pose T : subType _ := HB.pack equivQuotient [isSub for erepr]. by unlock pi; case=> x hx; apply/(@val_inj _ _ T)/eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)