proposition: Lemma CNF_psi_lt_Gamma0 p n: natp n -> CNF_psi_ax2 p n -> CNF_psiv p n <o Gamma_0.
proof: Proof. rewrite /CNF_psiv/CNFrv. have gl:= Gamma0_limit. move: n; apply: Nat_induction. by move => _; rewrite osum_f0; move/limit_pos: gl. move => n nN Hrec [[h1 h2] h3]. have nn:=(cltS nN). move: (indecomp_prop4 (proj31 gl)); rewrite Gamma0_epsilon. rewrite /CNF_psiv /CNFrv (osum_fS _ nN). have: CNF_psi_ax2 p n. split; first split. + move => i lin; apply: h1 (clt_ltT lin nn). + move => i iN slin; apply: h2 iN (clt_ltT slin nn). + move => i lin; apply:h3 (clt_ltT lin nn). move /Hrec; apply: indecomp_prop2. move: (h3 _ nn) => [sa sb]. move: (Gamma0_s_psi sa sb); rewrite /CNF_from_psi. by rewrite (odegree_psi (proj31_1 sa) (proj31_1 sb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)