proposition: Lemma CNF_exponents_I e c n: natp n -> CNFq_ax e c n -> forall i j, i <c n -> j <c n -> e i = e j -> i = j.
proof: Proof. move => nN /(CNF_exponents_sM nN) => m i j lin ljn eq. case: (cleT_ell (proj31_1 lin) (proj31_1 ljn)) => cp. + exact. + by move: (proj2 (m i j cp ljn)); rewrite eq. + by move: (proj2 (m j i cp lin)); rewrite eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)