proposition: Lemma CNF_psi_p1 p n: CNF_psi_ax p n -> CNFr_ax (CNF_from_psi p) n.
proof: Proof. move => [ax1 ax2]; split. move => i lin; move: (ax1 _ lin) => [_ qa qb]. apply:(OS_degree (OS_Spsi qa qb)). move => i iB lin. move: (ax1 _ (cle_ltT (cleS iB) lin)) => [_ qc qd]. move: (ax1 _ lin) => [_ qa qb]; rewrite /CNF_from_psi. move: (odegree_psi qa qb) (odegree_psi qc qd) => eq1 eq2. move:(ax2 i iB lin); rewrite /Spsip -{1} eq1 - {1} eq2 => h. move:(OS_degree (OS_Spsi qa qb)) (OS_degree (OS_Spsi qc qd)) => o1 o2. by move/(opow_Mo_leP o2 o1):h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)