proposition: Lemma ext2_pr9 E E' g z z': bijection_prop g E E' -> inc z (partitions E) -> inc z' (partitions E) -> (extension_p3 g z) = (extension_p3 g z') -> z = z'.
proof: Proof. move => ha /Zo_S hb /Zo_S hc ea. by rewrite - (ext2_pr7 ha hb) - (ext2_pr7 ha hc) ea. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)