proposition: Lemma cnf_nc_prop y c (z := cnf_nc y c) : cnfp_nz y -> natp c -> [/\ cnfp z, domain z = domain y, forall i, i<c domain y -> oexp z i = oexp y i, forall i, i<c cnf_size y -> Vg z i = Vg y i & cnf_lc z = c +c cnf_lc y].
proof: Proof. move => ynz; move/cnfpP:(proj1 ynz) => [fgx nN qa qb] cN. have eq1: domain z = domain y by rewrite /z/cnf_nc; aw. have eq2: cnf_size z = cnf_size y by rewrite /cnf_size eq1. move: (cnf_size_nz_bis ynz) => ha. move: (cnf_size_nz ynz) => [dN dv]. have ->:cnf_lc z = c +c cnf_lc y. by rewrite {1}/cnf_lc eq2 /z/cnf_nc/cnf_c /ocoef/cnf_size LgV//; Ytac0; aw. have aux i: i <c cnf_size y -> Vg z i = Vg y i. rewrite /z/cnf_nc => ils; rewrite LgV //. by rewrite /cnf_c (Y_false (proj2 ils)). move /(NltP nN): ha => sd. by apply/(NltP nN); apply: (clt_ltT ils sd). have eq3:forall i, i<c domain y -> oexp z i = oexp y i. move => i; rewrite dv/oexp ; move/(cltSleP dN). case/cle_eqVlt => cpa; last by rewrite aux. by rewrite cpa /z/cnf_nc/cnf_c LgV//;Ytac0; aw. split => //. apply/cnfpP; split. - rewrite /z/cnf_nc; fprops. - by rewrite eq1. - move => i; rewrite eq1 => idy. move /(NltP nN): (idy); rewrite dv; move/(cltSleP dN). case/cle_eqVlt => cpa; last by rewrite (aux _ cpa); apply: qa. rewrite cpa /z /cnf_nc /cnf_c LgV//; Ytac0; split; aww. by apply: OS_cnf_degree. by apply:(posnat_add cN); case:(qa _ ha). - move => i iN;rewrite eq1 => lin. by rewrite (eq3 _ (clt_ltT (cltS iN) lin)) (eq3 _ lin); apply: qb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)