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