proposition: Lemma um_unitbUn f1 f2 : unitb (f1 \+ f2) = unitb f1 && unitb f2.
proof: Proof. rewrite /unitb !pcmE /= !umEX /UM.empb /UM.union. case: (UMC.from f1) (UMC.from f2)=>[|f1' F1][|f2' F2] //. - by rewrite andbF. case: ifP=>E; case: eqP=>E1; case: eqP=>E2 //; last 2 first. - by move: E2 E1; move/supp_nilE=>->; rewrite fcat0s; case: eqP. - by move: E1 E2 E; do 2![move/supp_nilE=>->]; case: disjP. - by move/supp_nilE: E2 E1=>-> <-; rewrite fcat0s eq_refl. have [k H3]: exists k, k \in supp f1'. - case: (supp f1') {E1 E} E2=>[|x s _] //. by exists x; rewrite inE eq_refl. suff: k \in supp (fcat f1' f2') by rewrite E1. by rewrite supp_fcat inE /= H3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)