proposition: Lemma pairing_valid : (forall x, valid (pfst x) = valid x) * (forall x, valid (psnd x) = valid x) * (forall x, valid (ppair x) = valid x).
proof: Proof. split=>[|x]; last by rewrite valid_psub andbT. split=>x; (case: (pprodP x)=>[->|V]; first by rewrite pairing_undef !tpcmE); by case/(valid_pvalE X)/andP: V (V)=>/= E1 E2 ->; rewrite ?(E1,E2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)