proposition: Lemma cnf_nck_prop2 x: cnfp_nz x -> cnf_nck x \1c = x.
proof: Proof. move => xnz; rewrite/cnf_nck. move:(posnat_lc xnz) => /proj1/CS_nat cl; rewrite (cprod1r cl). apply: fgraph_exten. - fprops. - exact (proj41 (proj1 xnz)). - by aw. - aw => i idx; rewrite /cnf_c LgV//; Ytac h => //. - by rewrite /cnf_lc /cnf_degree - h (proj43 (proj1 xnz) i idx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)