proposition: Lemma Exercise6_12f f n: natp n -> Ex6_12_ax f n -> Ex6_12_v f n = oprodf (fun z => (omega0 +o f(csucc z))) n.
proof: Proof. move => nN ax; rewrite (Exercise6_12d nN ax) /CNFpv1. Ytac nz; first by rewrite nz oprod_f0. move: (cpred_pr nN nz); set m := cpred n; move => [mB sv]. move: ax; rewrite sv; clear sv; move: m mB; clear n nN nz. have Ha:= OS_succ OS_omega. apply: Nat_induction. move:(proj2(Exercise6_12a NS1 (card1_nz))); rewrite - {2} succ_zero => H ax. move: (ax _ H) => sa. have os:= (OS_sum2 OS_omega (OS_nat (proj1 sa))). by rewrite succ_zero oprod_f1 succ_zero (Y_true (erefl \1c)) (oprod1r OS_omega) // oprod_f1 succ_zero // (Exercise6_12e sa). move => n nN Hrec ax. have snN := NS_succ nN; have ssnN := NS_succ snN. have ax2: Ex6_12_ax f (csucc n). move => i/(Nint1cP snN) [inz lein]; apply: ax; apply/(Nint1cP ssnN). split => //; exact: (cleT lein (cleS snN)). have nsn:= (proj2(cltS snN)). rewrite (oprod_fS _ snN) (oprod_fS _ snN) - (Hrec ax2) ! (oprod_fS _ nN). repeat Ytac0. set w1 := oprodf _ _. set w2 := oprodf _ _. have <- : w1 = w2. apply: (oprodf_exten nN) => i lein. move: (clt_leT lein (cleS nN)) => [_ nin]. Ytac h1; first by move: (csucc_inj (proj31_1 lein) (CS_succ n) h1). Ytac h2 => //. by move:(csucc_inj (proj31_1 lein) (proj32_1 lein) h2) (proj2 lein). move: (Exercise6_12a ssnN (@succ_nz (csucc n))) => [/ax [ua _] /ax sa]. rewrite (oprod1r OS_omega) - (Exercise6_12e sa). move: (CNFp_pr1 olt_01 sa); rewrite /CNFp_value1/CNFp_value2 oopow1 => ->. have ow1: ordinalp w1. apply:(OS_oprodf nN) => i lin; apply: OS_succ. apply:(OS_prod2 OS_omega); Ytac y; fprops. move :(cleSS(cleSS (proj1 lin))) => h1. have ii: inc (csucc (csucc i)) (Nint1c (csucc (csucc n))). apply/(Nint1cP ssnN); split => //; apply: succ_nz. exact (OS_nat (proj1 (ax _ ii))). have of1:=OS_nat ua. move: (OS_prod2 ow1 Ha) (OS_nat (proj1 sa)) => owa ofn. rewrite (oprodA ow1 Ha ofn) (oprodA of1 (OS_prod2 owa ofn) Ha). by rewrite (oprodA (OS_prod2 of1 owa) ofn Ha) (oprodA of1 owa ofn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)