proposition: Lemma pairing_undef : (pfst undef = undef) * (psnd undef = undef) * (forall x, ~~ valid x -> ppair x = undef).
proof: Proof. split; first by rewrite /pfst/psnd /= pval_undef. case=>a b Vab; case: (pprodP (ppair (a, b)))=>//. by rewrite valid_psub (negbTE Vab). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)