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