proposition: Lemma um_prime f1 f2 k v : C k -> f1 \+ f2 = pts k v -> f1 = pts k v /\ f2 = Unit \/ f1 = Unit /\ f2 = pts k v.
proof: Proof. move: f1 f2; apply: um_indf=>[f1|f2 _|k2 w2 f1 _ _ _ f X E]. - rewrite undef_join -(validPt _ v)=>W E. by rewrite -E in W; rewrite valid_undef in W. - by rewrite unitL=>->; right. have W : valid (pts k2 w2 \+ (f1 \+ f)). - by rewrite -(validPt _ v) -E -joinA in X. rewrite -[pts k v]unitR -joinA in E. move/(cancel2 W): E; case: ifP. - by move/eqP=>-> [->] /join0E [->->]; rewrite unitR; left. by move=>_ [_ _] /esym/unitbP; rewrite um_unitbPtUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)