proposition: Lemma nxE0 (n1 n2 : lnat) : n1 \+ n2 = up 0 -> (n1 = up 0) * (n2 = up 0).
proof: Proof. case: n1 n2=>[|n1][|n2] //; rewrite upE /ojoin /=. by case=>/eqP; rewrite addn_eq0=>/andP [/eqP -> /eqP ->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)