proposition: Lemma Exercise6_12c f g n: natp n -> Ex6_12_ax f n -> Ex6_12_ax g n -> Ex6_12_v f n = Ex6_12_v g n -> forall i, inc i (Nint1c n) -> f i = g i.
proof: Proof. move => nN pa pb eq. move: (Exercise6_12b pa nN) (Exercise6_12b pb nN) => h1 h2. move: (proj2 (CNFp_unique h1 h2 nN nN eq)) => h3. move => i /(Nint1cP nN) [eq1 lein]. case: (equal_or_not n \0c) => nz. by rewrite nz in lein; case:eq1; apply:cle0. move: (pr2_def (h3 n (cltS nN))); rewrite / Ex6_12_c; repeat Ytac0;move => sf1. move: (cpred_pr (NS_le_nat lein nN) eq1) => [sa sb]. case: (equal_or_not (cpred i) \0c) => piz; first by rewrite sb piz succ_zero. move: (cpred_pr sa piz) => [sa' sb']. have lt1: cpred i <c n by apply/(cleSltP sa); rewrite - sb. move: (clt_ltT (cpred_lt sa piz) lt1) => [/(cltSleP nN) lt2 eq2]. move: (pr2_def (h3 _ lt2)); rewrite / Ex6_12_c - sb' - sb. by move: (proj2 lt1) => lt3; repeat Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)