proposition: Lemma Exercise6_12b f n: Ex6_12_ax f n -> natp n -> CNFp_ax (Ex6_12_ec f n) n.
proof: Proof. move: OS0 olt_01 PN1 => qa qb ac pb nN. rewrite /Ex6_12_ec/Ex6_12_e /Ex6_12_c; split. move => i lin; rewrite (Y_false (proj2 lin)) (Y_false (proj2 lin)). split;aww; case: (equal_or_not (csucc i) n) => nsi; Ytac0=> //. have sin: csucc i <=c n by apply/(cleSlt0P (proj31_1 lin) nN). apply: pb; apply/(Nint1cP nN);split; first apply: succ_nz. by apply/(cleSlt0P (proj31 sin) nN). Ytac0; Ytac0; split;aww; Ytac b => //; apply: pb. exact: (proj1 (Exercise6_12a nN b)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)