proposition: Lemma Exercise6_6_32case2 A B k: Exercise6_32_hyp A B k -> natp k -> ~ (exists2 i, intp i & nonempty (Vg A i)) -> Exercise6_32_conc A B k.
proof: Proof. move => ha hb hc. case: (p_or_not_p (exists2 i : Set, intp i & nonempty (Vg B i))) => hd. by move: (Ex6_32p4d ha hb hd). move: (proj42 (proj41 ha)) (proj42 (proj42 ha)) => dA dB. case: (emptyset_dichot (unionb A)) => Ae; last first. move:(rep_i Ae) => /setUb_P; rewrite dA; move =>[y ya yb]. case: hc; exists y => //; ex_tac. case: (emptyset_dichot (unionb B)) => Be; last first. move:(rep_i Be) => /setUb_P; rewrite dB; move =>[y ya yb]. case: hd; exists y => //; ex_tac. exists empty_function; rewrite Ae Be; split. - move:empty_function_function =>[ea eb ec]. split => //; split;split => //. by rewrite eb => i j /in_set0. by rewrite ec => j /in_set0. - move => i x iz xx; case: hc; exists i => //; ex_tac. - move => i x iz xx; case: hd; exists i => //; ex_tac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)