proposition: Lemma xval_inj x y : xval x = xval y -> x = y.
proof: Proof. by case: x y=>x Hx [y Hy] /= E; subst y; rewrite (pf_irr Hx). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)