proposition: Lemma compose_bp E E' E'' g g': bijection_prop g E E' -> bijection_prop g' E' E'' -> bijection_prop (g' \co g) E E''.
proof: Proof. move=> [ha1 ha2 ha3] [hb1 hb2 hb3]. hnf; aw;split => //; apply: compose_fb => //; split; try fct_tac. by rewrite ha3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)