proposition: Lemma ptrT x y : {m : nat | (x == y.+m) || (y == x.+m)}.
proof: Proof. case: x y=>x [y]; exists (if x <= y then (y - x) else (x - y)). rewrite !ptrE leq_eqVlt /=. by case: (ltngtP x y)=>/= E; rewrite subnKC ?(ltnW E) ?eq_refl ?orbT // E. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)