proposition: Lemma partition_nq_pr6d E E' q: E \Eq E' -> (partition_nq E q) \Eq (partition_nq E' q).
proof: Proof. move => [g gp]. exists (Lf (extension_p3 g) (partition_nq E q) (partition_nq E' q)). hnf; aw; split => //; apply: lf_bijective. - by apply: partition_nq_pr6c. - move => u v /Zo_S /Zo_S ua /Zo_S /Zo_S va sv. by rewrite -(ext2_pr7 gp ua) -(ext2_pr7 gp va) sv. - move => y yp; move: (yp) => /Zo_S /Zo_S ypp. move: (gp) => [ha1 ha2 ha3]. move: (ext2_pr7 (inverse_bij_bp gp) ypp) (partition_nq_pr6c (inverse_bij_bp gp) yp). rewrite (ifun_involutive (proj1 (proj1 ha1))) =>{2} <- h; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)