proposition: Lemma In_range_omapUn (a : K*V -> option V') f1 f2 x : x \In range (omap a (f1 \+ f2)) <-> valid (f1 \+ f2) /\ (x \In range (omap a f1) \/ x \In range (omap a f2)).
proof: Proof. split. - case W : (valid (f1 \+ f2)); first by rewrite omapUn // => /In_rangeUn. by move/negbT/invalidE: W=>->; rewrite omap_undef range_undef. case=>W H; rewrite omapUn //; case: H=>H. - by apply: In_rangeL H; rewrite -omapUn // valid_omap. by apply: In_rangeR H; rewrite -omapUn // valid_omap. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)