proposition: Lemma ext2_pr6 E E' E'' g g' z: bijection_prop g E E' -> bijection_prop g' E' E'' -> inc z (\Po (\Po E)) -> extension_p3 g' (extension_p3 g z) = extension_p3 (g' \co g) z.
proof: Proof. move => ha hb zz. have hc:=(compose_bp ha hb). move:(ha) (hb)=> [ha1 ha2 ha3] [hb1 hb2 hb3]. move: (ext2_pr5 ha zz); rewrite (ext2_pr2 ha zz) => hd. have he: composableC g' g. by apply: composable_for_function;split; try fct_tac; rewrite ha3. have hf:composableC (extension_to_parts g') (extension_to_parts g). have ra:=(proj31 (etp_f (proj31 (proj1 (proj1 ha1))))). have rb:=(proj31 (etp_f (proj31 (proj1 (proj1 hb1))))). by split => //; rewrite lf_source lf_target hb2 ha3. have zz': inc z (source (extension_to_parts (extension_to_parts g))). by rewrite !lf_source ha2. rewrite (ext2_pr2 hc zz) (ext2_pr2 hb hd). rewrite /extension_p2 (etp_compose he) etp_compose // compfV//. by apply:etp_composable. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)