proposition: Lemma hist_path A (h : natmap A) : path oleq 0 (dom h).
proof: Proof. rewrite !umEX; case: (UMC.from h)=>//= {}h _; case: h; case=>//= x s H. rewrite {1}/oleq /ord /= orbC -leq_eqVlt /=. by apply: sub_path H=>z y; rewrite /oleq=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)