proposition: Fact r2v_subproof : {r2v | cancel r2v v2r}.
proof: Proof. have r2vP r: {v | v2r v = r}. by apply: sig_eqW; have [v _ vK] := v2r_bij; exists (v r). by exists (fun r => sval (r2vP r)) => r; case: (r2vP r). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)