proposition: Lemma nxV (m1 m2 : lnat) : valid (m1 \+ m2) -> exists n1 n2, m1 = up n1 /\ m2 = up n2.
proof: Proof. by case: m1=>// n1; case: m2=>// n2; exists n1, n2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)