proposition: Lemma partition_nq_pr6c E E' q g: bijection_prop g E E' -> lf_axiom (extension_p3 g) (partition_nq E q) (partition_nq E' q).
proof: Proof. move => bg z /Zo_P [za zb]; apply:(Zo_i (ext2_pr8 bg za)). move:za => /Zo_P [ zz zc]. move => x /(ext2_pr3 bg zz) [u uz ->]. move:(bg) => [[ig _] sg _]. have usg: sub u (source g) by rewrite sg;apply/setP_P; move/setP_P:zz; apply. rewrite (cardinal_image usg ig); exact: (zb _ uz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)