proposition: Lemma position_in_cnf_prop2 x i: cnfp x -> inc i (domain x) -> position_in_cnf x (oexp x i) = i.
proof: Proof. move=> ox pb. move/cnfpP: (ox) => /proj43 h; move: (proj32 (h _ pb)) => od. move: (position_in_cnf_prop ox od); set k := position_in_cnf _ _. move => [ka kb kc]. have nN:= (proj42 ox). move/(NltP nN): pb => idx. move:(NS_lt_nat idx nN) => iN. case: (cleT_ell (proj31 ka) (CS_nat iN)); [exact | | by move/kb; case]. move => lik. case: kc; first by move => ea; case:(proj2 (clt_ltT lik idx)). case/oleNgt. exact: (CNF_exponents_sM (proj42 ox) (proj1 (proj44 ox)) lik idx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)