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