proposition: Lemma Ex6_32p4a' A B k0 n: Exercise6_32_hyp A B k0 -> natp k0 -> intp n -> Vg (fdfc A) (BZsucc n) <=c csumb (ZN_int n k0 (\1c +c k0)) (Vg (fdfc B)).
proof: Proof. move => [ha hb hc hd] kN nz. move:(ZS_succ nz) => q. have h: cardinalp (Vg (fdfc A) (BZsucc n)) by rewrite /fdfc /fin_disj_fam_card; bw; fprops. exact: (cleT (Ex6_32p3' nz h) (hc _ _ nz NS1 (cleR CS1))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)