proposition: Lemma left_compose_fb f f': f' \coP f -> bijection (f' \co f) -> bijection f -> bijection f'.
proof: Proof. move=> cff bc bf; move: (inverse_bij_fb bf) => bf'. rewrite -(compf_rK bf cff); apply: compose_fb => //; saw; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)