proposition: Lemma compose_fb f f': bijection f -> bijection f' -> f' \coP f -> bijection (f' \co f).
proof: Proof. by move=> [inf sf] [inf' sf']; split ; [apply: compose_fi | apply: compose_fs]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)