proposition: Lemma CNF_psi_p0 p n: CNF_psi_ax p n -> natp n -> CNF_psiv p n = osumf (fun i => (Spsip (p i))) n.
proof: Proof. move => [a1 a2] nN. apply: (osumf_exten nN) => i lin. move: (a1 _ lin) => [_ pb pc];exact (odegree_psi pb pc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)