proposition: Lemma NS_Vr x e: cnfp x -> natp (Vr x e).
proof: Proof. move => ox. case: (p_or_not_p (inc e (domain (range x)))); last first. rewrite /Vr; move/Vg_out_of_range => ->; apply: NS0. by move /(Vr_posnat ox) => /proj1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)