proposition: Lemma cnf_range_fgraph x: cnfp x -> fgraph (range x).
proof: Proof. move => ax; move: (ax) => [fgx nN ha hb]. split. by move => i /(range_gP fgx) [n /ha px -> ]. move => i j /(range_gP fgx) [n nds ->] /(range_gP fgx) [m mds ->] sp. by rewrite (cnf_monomial_inj ax nds mds sp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)