proposition: Lemma Ex6_32p4b' A B k0 i: Exercise6_32_hyp A B k0 -> natp k0 -> intp i -> (forall k, k <=z i -> Vg (fdfc A) k = \0c) -> forall k, k <=z i -z (ZN k0) -> Vg (fdfc B) k = \0c.
proof: Proof. move => /Ex6_32_HS Hab kN zi H k k1. have kz := (proj31 k1). move: (Ex6_32p4a' Hab kN (ZS_pred kz)); rewrite /csumb; set s := csum _. rewrite (BZsucc_pred kz). suff: s = \0c by move => -> /cle0. have k0z := ZNz kN. have k2: k +z ZN k0 <=z i. move/(BZsum_le2r kz (proj32 k1) k0z): k1. by rewrite BZsum_diff1. apply / csum_zero_unit_bis => j; aw => jj; bw => //. move /(ZN_intP (ZS_pred kz) kN (NS_sum NS1 kN)): jj => /proj2. rewrite - (BZsum_cN NS1 kN) (BZsumA (ZS_pred kz) ZS1 k0z). rewrite -/(BZsucc _) (BZsucc_pred kz) => ww. by apply: H; move: (zleT ww k2). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)