proposition: Lemma right_pf h r (f : forall k, partition k r) k : partition_axiom k (h \+ r) (right_tag (h \+ f k)).
proof: Proof. by rewrite partitionE /partition_axiom /= joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)