proposition: Lemma cnfp_cnf_ns x k: cnfp x -> k <=c domain x -> cnfp (cnf_ns x k).
proof: Proof. move => /cnfpP [ha hb hc hd] lk; rewrite /cnf_ns; apply/cnfpP. rewrite Lgd. move:(NS_diff k hb); set m := _ -c _ => mN. move: (NS_le_nat lk hb) => kN. have H i: i <c m -> i +c k <c domain x. by move/(csum_Mlteq kN); rewrite(csumC m) (cdiff_pr lk). split. - fprops. - exact. - by rewrite /cnf_s;move => i im; rewrite LgV//; apply: hc; apply/(NltP hb)/H /(NltP mN). - rewrite/cnf_s/oexp;move => i iN idx. move/(NltP mN):(idx)=> idx1. move/(NltP mN):(clt_ltT (cltS iN) idx) => ik. rewrite !LgV// (csum_Sn _ iN); apply:(hd _ (NS_sum iN kN)). by rewrite -(csum_Sn _ iN); apply: H; apply/(NltP mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)