proposition: Lemma inj_compose1 f f': injection f -> injection f' -> source f' = target f -> injection (f' \co f).
proof: Proof. move=> injf injf' sff';apply: compose_fi=> //;split => //; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)