proposition: Lemma CNFB_monomial_inj x (z := (the_CNFB b x)): ordinalp x -> {when inc ^~ (domain z) & , injective (oexp z)}.
proof: Proof. move => ox; move:(the_CNF_p0 bg2 ox) => [[fgz nN pz ax] _] i j idx jdx sv. move: (CNF_exponents_sM nN (proj1 ax)) => M. case: (NleT_ell (NS_inc_nat nN idx) (NS_inc_nat nN jdx)). - by move ->. - move => lij; move/(NltP nN): jdx => jdx. by case:(proj2(M _ _ lij jdx)). - move => lij; move/(NltP nN): idx => idx. by case:(proj2(M _ _ lij idx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)