proposition: Lemma Ex6_32p4d A B k0: Exercise6_32_hyp A B k0 -> natp k0 -> (exists2 i, intp i & nonempty (Vg B i)) -> exists2 i, intp i & nonempty (Vg A i).
proof: Proof. move => ha hb [i iz /card_nonempty1 nai]; move: (ZNz hb) => kz. case:(all_exists_dichot2 (fun j => nonempty (Vg A j)) BZ) => // H. have h: forall j, j <=z i +z (ZN k0) -> (Vg (fdfc A) j) = \0c. move => j /proj31 jz; rewrite (LgV jz); move:(H j jz) => /nonemptyP. by case: (equal_or_not (Vg A j) emptyset) => // -> _; rewrite cardinal_set0. case: nai;move:(Ex6_32p4b' ha hb (ZSs iz kz) h). rewrite (BZdiff_sum1 kz iz) => h1. by move: (h1 _ (zleR iz)); rewrite (LgV iz). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)