proposition: Lemma CNF_exponents_sM e c n: natp n -> CNFq_ax e c n -> forall i j, i <c j -> j <c n -> e i <o e j.
proof: Proof. move => nN ax i j lij ljn. have iN := (NS_lt_nat (clt_ltT lij ljn) nN). move /(cleSltP iN) :lij => leij. have sa:=(CNF_exponents_M nN ax leij ljn). move: ax => [_ _ _ ax]; exact: (olt_leT (ax i iN (cle_ltT leij ljn)) sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)