proposition: Lemma ord_negl_pg (f:fterm) n (g:fterm) m: natp n -> CNFr_ax f (csucc n) -> natp m -> CNFr_ax g (csucc m) -> (g m <o f n <-> CNFrv g (csucc m) <<o CNFrv f (csucc n)).
proof: Proof. move=> nN cf mN cg; split. rewrite (CNFr_rec _ nN) => t2. have p2: ordinalp (omega0 ^o f n) by apply:(OS_pow OS_omega (proj32_1 t2)). have p3 := (OS_CNFr0 nN (CNFr_ax_s nN cf)). apply: (ord_negl_sum (OS_CNFr0 (NS_succ mN) cg) p2 p3). move: m mN cg t2;apply: Nat_induction. rewrite succ_zero => ax1 lt1. have h0:= (OS_pow OS_omega(proj31_1 lt1)). by rewrite /CNFrv (osum_f1 (f:= oopow \o g) h0);apply:ord_negl_p4. move => m mN Hrec cdg ltspd. move: OS_omega (NS_succ mN) => oo smN. rewrite (CNFr_rec _ smN). have ax2:= (CNFr_ax_s smN cdg). have o1:= (OS_pow oo (proj31_1 ltspd)). apply/(ord_negl_sum1 o1 (OS_CNFr0 smN ax2) p2); split. by apply: (ord_negl_p4). apply: Hrec => //. exact : (ole_ltT (proj2 cdg m mN (cltS smN)) ltspd). rewrite (CNFr_rec _ mN) => t2. have ax2:= (CNFr_ax_s mN cg). have o0:= (proj1 cg _ (cltS mN)). have o2:= (proj1 cf _ (cltS nN)). have o1:= (OS_pow OS_omega o0). have o4:=(OS_CNFr0 (NS_succ nN) cf). move:(ord_negl_sum1 o1 (OS_CNFr0 mN ax2) o4). move/(ord_negl_sum1 o1 (OS_CNFr0 mN ax2) o4):t2 => [/(ord_negl_alt o1 o4)]. rewrite - (opow_succ OS_omega o0) => ha _. move:(ole_ltT ha (CNFr_p4 nN cf)). by move/(opow_Meqltr ole_2omega (OS_succ o0) (OS_succ o2))=>/oltSSP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)