proposition: Lemma prec_domV x1 x2 y1 y2 : valid (x1 \+ y1) -> x1 \+ y1 = x2 \+ y2 -> reflect {subset dom x1 <= dom x2} (valid (x1 \+ y2)).
proof: Proof. move=>V1 E; case V12 : (valid (x1 \+ y2)); constructor. - move=>n Hs; have : n \in dom (x1 \+ y1) by rewrite domUn inE V1 Hs. rewrite E domUn inE -E V1 /= orbC. by case: validUn V12 Hs=>// _ _ L _ /L /negbTE ->. move=>Hs; case: validUn V12=>//. - by rewrite (validE2 V1). - by rewrite E in V1; rewrite (validE2 V1). by move=>k /Hs; rewrite E in V1; case: validUn V1=>// _ _ L _ /L /negbTE ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)