proposition: Lemma Ex6_32p6 A B k0 q: Exercise6_32_hyp A B k0 -> natp k0 -> intp q -> supp_left_unbounded (fdfc A) -> supp_right_unbounded (fdfc A) -> bijection_prop (Ex6_32_fctL_gen A B q) (unionb A) (unionb B).
proof: Proof. move => ha kz qz hb hc. move: (ha) =>[Ap Bp relA relB]. move: (Ex6_32p5a ha kz hb hc) =>[rA rB]. rewrite /Ex6_32_fctL_gen; split; aw => //. apply: lf_bijective. - move => t tu. rewrite /Ex6_32_fctL_aux. move: (ZSs (Zo_S (fin_disj_fam_enum_range_p1 Ap tu)) qz). rewrite /intp - rB => aux; exact: (proj2 (fdfe_inv_prop Bp aux)). - move => u v uua vua. move: (Zo_S (fin_disj_fam_enum_range_p1 Ap uua)) => pu. move: (Zo_S (fin_disj_fam_enum_range_p1 Ap vua)) => pv. move: (ZSs pu qz) (ZSs pv qz); rewrite /intp - rB => pu1 pv1. move: (fdfe_inv_prop Bp pu1) (fdfe_inv_prop Bp pv1). rewrite /Ex6_32_fctL_aux; set a := fdfe_inv B _; set b := fdfe_inv B _. move =>[ra rb] [rc rd] eab. move: rc; rewrite - eab ra => /(BZsum_eq2r pu pv qz). by move/(fin_disj_fam_prop6 Ap uua vua). move => y yub. move: (Zo_S (fin_disj_fam_enum_range_p1 Bp yub)) => pu. move:(ZS_diff pu qz); rewrite /intp - rA. set i := _ -z _; move/Zo_P =>[iz [x xu iv]]. exists x => //. rewrite /Ex6_32_fctL_aux /fdfe iv /i (BZsum_diff1 qz pu). rewrite - rB in pu. move: (fdfe_inv_prop Bp pu) =>[wa wb]. by move/(fin_disj_fam_prop6 Bp wb yub): wa. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)