proposition: Lemma ext2_pr8 E E' g z: bijection_prop g E E' -> inc z (partitions E) -> inc (extension_p3 g z) (partitions E').
proof: Proof. move => pa /Zo_P [ha [[hb hc] hd]]. move:(pa) => [[[fg ig] [_ sjg]] sg tg]. move/setP_P: (ha) => ha'. have K a b: inc b z -> inc a b -> inc a (source g). by move => sa sb; rewrite sg - hb; union_tac. have H x: inc x z -> forall y, inc y (Vfs g x) <-> (exists2 u, inc u x & y = Vf g u). move => /ha' /setP_P; rewrite - sg => tt. exact:(Vf_image_P fg tt). apply: (Zo_i (ext2_pr5 pa ha)); split; last first. move => t /(ext2_pr3 pa ha) [u uz ->]. move:(hd _ uz) => [v vu]; exists (Vf g v); apply/(H _ uz); ex_tac. split => //. set_extens t. move/setU_P => [y yz /(ext2_pr3 pa ha) [u uz yv]]. move: yz; rewrite yv => /(H _ uz) [w /(K _ _ uz) wu ->]; Wtac. rewrite - tg => /sjg [x xsg ->]; apply /setU_P. move: xsg; rewrite sg - hb => /setU_P [v xv vz]. exists (Vfs g v); first by apply/(H _ vz); ex_tac. by apply/(ext2_pr3 pa ha); ex_tac. move => a b /(ext2_pr3 pa ha) [u uz ->] /(ext2_pr3 pa ha) [v vz ->]. case: (hc _ _ uz vz) => uv; [ by rewrite uv; left | right ]. apply: disjoint_pr => x /(H _ uz) [u' uu' ->] /(H _ vz) [v' vv' ea]. by empty_tac1 u'; rewrite (ig _ _ (K _ _ uz uu') (K _ _ vz vv') ea). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)