proposition: Lemma CNFB_range_fgraph x : ordinalp x -> fgraph (range (the_CNFB b x)).
proof: Proof. move => ox. move:(the_CNF_p0 bg2 ox) => [[fgz nN pz ax] _]. split; first by move => t/(range_gP fgz) [i /pz pp ->]. move => i j /(range_gP fgz) [n nds ->] /(range_gP fgz) [m mds ->] sp. by rewrite (CNFB_monomial_inj ox nds mds sp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)