proposition: Lemma Ex6_32p5e A B k0: Exercise6_32_hyp A B k0 -> natp k0 -> (exists2 i, intp i & nonempty (Vg A i)) -> ~ supp_left_unbounded (fdfc A) -> ~supp_right_unbounded (fdfc A) -> zint_k5 (fdfer A) /\ zint_k5 (fdfer B).
proof: Proof. move => ha hb hc hd he. move:(ha) =>[qa qb _ _]. move: (Ex6_32p4d (Ex6_32_HS ha) hb hc) => hc'. split; apply:fin_disj_fam_prop10e => //. by apply: (Ex6_32p4c1 ha hb hd). by apply: (Ex6_32p4c2 ha hb he). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)