proposition: Lemma pos_joinA x y z : pos_join x (pos_join y z) = pos_join (pos_join x y) z.
proof: Proof. by apply/eqP; rewrite /pos_join -val_eqE /= maxnA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)