proposition: Lemma CNF_exponents_M 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 [_ pb _ pc] i j lij ljn. have lin:=(cle_ltT lij ljn). have iN := (NS_lt_nat lin nN). pose r j := e i <=o e j. have ri:=(oleR (pb _ lin)). case: (equal_or_not n \0c) => nz. by move: lin; rewrite nz; move /clt0. move: (cpred_pr nN nz) => [mN mv]. have jcn: j <=c cpred n by apply /(cltSleP mN); rewrite -mv. move: (Nat_induction3 (r := r) iN mN ri)=> h. apply: (h _ j lij jcn) => k ik kn; rewrite /r => le1. have kN:= (NS_lt_nat kn mN). have skn : csucc k <c n. by rewrite mv; apply/(cltSleP mN) /(cleSltP kN). by move:(pc k kN skn) => [ /(oleT le1) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)