proposition: Lemma partition_nq_pr8 E q x y: natp q -> q <> \0c -> inc x (partition_nq E q) -> inc y (partition_nq E q) -> exists2 f, inc f (permutations E) & Vfs (extension_to_parts f) x = y.
proof: Proof. move => qN qp xp yp. move:(partition_nq_pr1 yp) => ha. move:(partition_nq_pr2 (CS_cardinal y) qN qp ha xp) => /card_eqP [f [bf sf tf]]. move:(xp) => /Zo_P [/Zo_P [_ [/partition_same ra]]] _ _. move:xp => /Zo_P [ /Zo_P [pa [[pb pc] pd]] pe]. move:yp => /Zo_P [ /Zo_P [qa [[qb qc] qd]] qe]. pose h1 i := equipotent_ex i (Vf f i). have ff: function f by fct_tac. have h1p: forall i, inc i x -> bijection_prop (h1 i) i (Vf f i). move => i ix; apply:equipotent_ex_pr. apply/card_eqP; rewrite (pe _ ix) qe //; Wtac. pose h i:= Lf (Vf (h1 i)) i E. have rb': forall i j, inc i x -> inc j i -> inc (Vf (h1 i) j) E. move => i j ix ij; move:(h1p _ ix) => [[[fa _] _] sa ta]. rewrite - qb; apply /setU_P; exists (Vf f i); Wtac; fct_tac. have rb: (forall i, inc i (domain (identity_g x)) -> function_prop (h i) (Vg (identity_g x) i) E). rewrite identity_d => i ix; rewrite (identity_ev ix) /h; hnf;aw. by split => //; apply:lf_function => j ji; apply: rb'. move:(extension_partition1 ra rb); set g:= common_ext _ _ _. move => [[fg sg tg] rc]. have rc': forall i, inc i x -> agrees_on i g (h i). by move => i ix;move: (rc i); rewrite identity_d (identity_ev ix); apply. have rc'': forall i j, inc i x -> inc j i -> Vf g j = Vf (h1 i) j. move => i j ix ij; move: (rc' _ ix) => [sa sb sc]; rewrite (sc j ij). by rewrite /h LfV//; move => t ti; apply: rb'. have rd: injection g. split => //; rewrite sg -pb => u v /setU_P [xa uxa xax] /setU_P [xb vxb xbx]. rewrite (rc'' _ _ xax uxa) (rc'' _ _ xbx vxb) => eq1. have sa: inc (Vf (h1 xa) u) (Vf f xa). move:(h1p _ xax) => [[[fa _] _] sa sb]; Wtac. have sb: inc (Vf (h1 xb) v) (Vf f xb). move:(h1p _ xbx) => [[[fa _] _] sa' ta]; Wtac. have sc: inc (Vf f xa) y by Wtac. have sd: inc (Vf f xb) y by Wtac. case:(qc _ _ sc sd)=> ea; last by empty_tac1 (Vf (h1 xa) u); rewrite eq1. move: (proj2 (proj1 bf)); rewrite sf => iif; move: (iif _ _ xax xbx ea) => eb. rewrite eb in eq1 uxa. move:(h1p _ xbx)=> [[[_ se] _] sh th]; apply:se;rewrite ? sh //. have re: surjection g. split => //; rewrite sg tg - {1} qb => t /setU_P [s ts sy]. rewrite - tf in sy; move: (proj2 (proj2 bf) _ sy) => [u usf sv]. rewrite sf in usf. move:(h1p _ usf) => [[_ [_ ssa]] sa ta]. have: inc t (target (h1 u)) by rewrite ta - sv. move/ssa; rewrite sa; move => [w wu ->]; exists w. rewrite - pb; union_tac. by rewrite (rc'' _ _ usf wu). have bpg: bijection_prop g E E by []. have rf: inc g (permutations E) by apply/permutationsP. ex_tac. have ti: forall u, inc u x -> Vfs g u = Vf f u. move => u ux; move:(h1p _ ux) => [[ba [fh sh]] sa <-]. have su: sub u (source g) by rewrite sg; apply/setP_P; move/setP_P:pa; apply. set_extens t. move /(Vf_image_P fg su) => [v uv ->]; rewrite (rc'' _ _ ux uv); Wtac. move/sh; rewrite sa;move => [v vx ->]; apply/(Vf_image_P fg su). by ex_tac; rewrite (rc'' _ _ ux vx). set_extens t. move/(ext2_pr3 bpg pa) => [u ux ->]. rewrite (ti _ ux) - tf; Wtac. rewrite -tf; move/(proj2 (proj2 bf)); rewrite sf; move => [u ux ->]. by apply/(ext2_pr3 bpg pa); ex_tac; rewrite - (ti _ ux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)