proposition: Lemma Ex6_32pk0 A B: Exercise6_32_hyp A B \0c -> forall n, intp n -> Vg A n =c Vg B n.
proof: Proof. move => [Ap Bp Ha Hb] n nz. have ra: forall f m, intp m -> csumb (ZN_int m \0c \2c) f = (f m +c f (BZsucc m)) +c f (BZsucc (BZsucc m)). move => f m mz. have eq1: m +z (ZN \2c) = (BZsucc (BZsucc m)). by rewrite /BZsucc - (BZsumA mz ZS1 ZS1) (BZsum_cN NS1 NS1) csum_11. set I := (ZN_int m \0c \1c). move: (zlt_succ mz) => la. move: (proj1 (zlt_succ (ZS_succ mz))) => lb. have Is: ~ inc (BZsucc (BZsucc m)) I. move/(ZN_intP mz NS0 NS1) =>[_ ]. by move/(zleSSP (ZS_succ mz) mz); apply: zltNge. have ->: (ZN_int m \0c \2c) = I +s1 (BZsucc (BZsucc m)). set_extens t. move/(ZN_intP mz NS0 NS2) =>[qa]; rewrite eq1; case/zle_eqVlt. move ->; apply: setU1_1. move/(zlt_succ1P (proj32 qa) (ZS_succ mz)) => qb. by apply: setU1_r; apply(ZN_intP mz NS0 NS1). move => h; apply /(ZN_intP mz NS0 NS2); rewrite eq1. case/setU1_P:h. move/(ZN_intP mz NS0 NS1) => [qa qb]; split => //; exact: (zleT qb lb). move ->; split; last exact:(zleR (ZS_succ (ZS_succ mz))). rewrite (Ex6_32p0 mz); exact: (zleT (proj1 la) lb). by rewrite (csumA_setU1 _ Is) (Ex6_32p2 _ mz). pose Ac := (fin_disj_fam_card A). pose Bc := (fin_disj_fam_card B). have rb m: intp m -> csumb (ZN_int m \0c \2c) (Vg Ac) = csumb (ZN_int m \0c \2c) (Vg Bc). move => mz. move:(Ha m \2c mz NS2 (proj1 clt_12)) (Hb _ _ mz NS2 (proj1 clt_12)). by rewrite (csum0r CS2);apply: cleA. have rc m: intp m -> csumb (ZN_int m \0c \1c) (Vg Ac) = csumb (ZN_int m \0c \1c) (Vg Bc). move => mz. move:(Ha _ _ mz NS1 (cleR CS1)) (Hb _ _ mz NS1 (cleR CS1)). by rewrite (csum0r CS1);apply: cleA. move: (ZS_pred (ZS_pred nz)) (ZS_pred nz) => mz smz. move: (rc _ mz) (rb _ mz). rewrite (ra _ _ mz) (ra _ _ mz) (Ex6_32p2 _ mz) (Ex6_32p2 _ mz). move ->. rewrite (BZsucc_pred smz) (BZsucc_pred nz). set v := (Vg Bc (BZpred (BZpred n)) +c Vg Bc (BZpred n)). move: (fin_disj_fam_prop2 Bp) => [qa qb qc]. have vN: natp v by apply:NS_sum; apply:qc; rewrite qb. have Ann: natp (Vg Ac n). case: (fin_disj_fam_prop2 Ap) => [sa sb sc]; apply: sc; ue. have Bnn: natp (Vg Bc n) by apply: qc; ue. by move/(csum_eq2l vN Ann Bnn); rewrite /Ac /Bc /fin_disj_fam_card; bw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)