proposition: Lemma fresh0N h x : fresh h <= x -> x != 0.
proof: Proof. by case: eqP=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)