proposition: Lemma Vr_correct x i: cnfp x -> inc i (domain x) -> Vr x (oexp x i) = (ocoef x i).
proof: Proof. move => ox idx. move: (ox) => [ha hb hc hd]. symmetry; exact:(pr2_V (cnf_range_fgraph ox) (inc_V_range ha idx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)