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