proposition: Lemma cnf_monomial_inj x: cnfp x -> {when inc ^~ (domain x) & , injective (oexp x)}.
proof: Proof. move => ox i j idx jdx sv; move:(proj42 ox) => nN. move: (CNF_exponents_sM (proj42 ox) (proj1(proj44 ox))) => 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)