proposition: Lemma cnfp_cnf_nm x y: cnfp x -> cnfp y -> cnf_all_smaller x y -> cnfp (cnf_nm x y).
proof: Proof. move => /cnfpP [ha hb hc hd] /cnfpP [ha' hb' hc' hd'] aux. rewrite /cnf_nm /cnf_m; apply/cnfpP. rewrite Lgd; move:(NS_sum hb hb'); set m := _ +c _ => mN. have Hp i: i <c m -> domain x <=c i -> i -c domain x <c domain y. move => lt1 le2; apply: (cdiff_Mlt hb' (NS_lt_nat lt1 mN) le2). by rewrite csumC. split. - fprops. - exact. - move => i lim; rewrite LgV//; move /(NltP mN):lim=> lim. case: (cleT_el (CS_nat hb) (proj31_1 lim)) => cp1. by rewrite(Y_false (cleNgt cp1)); apply: hc'; apply/(NltP hb'); apply: Hp. by Ytac0; apply: hc; apply/NltP. rewrite/oexp; move => i iN idx. move/(NltP mN):(idx)=> idx1. move/(NltP mN):(clt_ltT (cltS iN) idx) => ik. have ii := (cltS iN). rewrite !LgV//. case: (NleT_el hb (NS_succ iN)) => cp1; last first. by rewrite(Y_true (clt_ltT ii cp1)); Ytac0; apply: (hd _ iN cp1). rewrite (Y_false (cleNgt cp1)); case/cle_eqVlt: cp1 => cp2. rewrite cp2 (Y_true ii) cdiff_nn; apply: aux; first by rewrite cp2. apply/(strict_pos_P1 hb') => dyz. by move:(proj2 idx); rewrite /m dyz cp2 (csum0r (CS_succ _)). move/(cltSleP iN): cp2 => cp2; rewrite (Y_false (cleNgt cp2)). move: (Hp _ idx (cleT cp2 (proj1 ii)));rewrite (cdiffSn iN cp2) => cp3. exact: (hd' _ (NS_diff (domain x) iN) cp3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)