proposition: Lemma pcmPJ (x1 y1 : U) (x2 y2 : V) : (x1, x2) \+ (y1, y2) = (x1 \+ y1, x2 \+ y2).
proof: Proof. by rewrite pcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)