proposition: Lemma nxPJ n1 n2 : nxownjoin_spec n1 n2 (nxown (n1 \+ n2)).
proof: Proof. case: n1 n2=>[|n1][|n2] /=. - by constructor. - by apply: (@nxjS _ _ n2). - by apply: (@nxjS _ _ n1); rewrite addn0 //. apply: (@nxjS _ _ (n1 + n2).+1). by rewrite addSn addnS. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)