proposition: Lemma nbpart_pr1 E F g p: bijection_prop g E F -> bijection (Lf (extension_p3 g) (partitionsx E p)(partitionsx F p)).
proof: Proof. move => pg. have T: forall X X' f z, bijection_prop f X X' -> inc z (partitionsx X p) -> inc (extension_p3 f z) (partitionsx X' p). move => X X' f z h /Zo_P [zp cz]; apply/Zo_P; split. apply: (ext2_pr8 h zp). rewrite - cz; symmetry; apply /card_eqP. exists (Lf ( Vf (extension_to_parts f)) z (extension_p3 f z)). move:(h) => [ha1 ha2 ha3]. have fg := (proj1 (proj1 ha1)). have cg := (proj31 fg). move: (etp_f cg) => ef. move:(zp) => /Zo_P [/setP_P qa qb]. have sz: sub z (source (extension_to_parts f)) by rewrite lf_source ha2. hnf; saw; apply:lf_bijective. - move => t tz; apply/(Vf_image_P ef sz); ex_tac. - by move => u v uz vz; apply: (proj2 (etp_fi (proj1 ha1))); apply: sz. - by move => y /(Vf_image_P ef sz). apply: lf_bijective. - by move => z; apply:T. - by move => u v /Zo_S ha /Zo_S hb; apply:(ext2_pr9 pg). - move => y yp. move:(T _ _ _ _ (inverse_bij_bp pg) yp) => xi; ex_tac. rewrite -{1} (ifun_involutive (proj1 (proj1 (proj31 pg)))). symmetry; apply: (ext2_pr7 (inverse_bij_bp pg) (Zo_S (Zo_S yp))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)