proposition: Lemma Vr_posnat x e: cnfp x -> inc e (cnf_exponents x) -> posnatp (Vr x e).
proof: Proof. move=> ox;move: (ox) => /cnfpP [ax _ hb _]. move/funI_P => [z /(range_gP ax) [i idx -> ] ->]. rewrite (Vr_correct ox idx). exact: (proj33 (hb _ idx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)