proposition: Lemma psub_inj x y : valid (psub x) -> psub x = psub y -> x = y.
proof: Proof. move=>W E; move: (W) (W). rewrite {1}E !valid_psub=>/andP [W2 H2] /andP [W1 H1]. have : pval (psub x) = pval (psub y) by rewrite E. by rewrite !pval_psub. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)