proposition: Lemma cnfp_cnf_nr x k: cnfp x -> k <=c domain x -> cnfp (cnf_nr x k).
proof: Proof. move => /cnfpP [ha hb hc hd] lk; rewrite /cnf_nr; apply/cnfpP. rewrite restr_d; move: (NS_le_nat lk hb) => kN. split; [ fprops | done | move => i idx | move => i iN idx]. rewrite LgV//; exact:(hc _ (proj33 lk _ idx)). move/(NltP kN):(idx)=> idx1. move/(NltP kN):(clt_ltT (cltS iN) idx) => ik. rewrite/oexp ! LgV//; apply: (hd _ iN (clt_leT idx lk)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)