proposition: Lemma composeC_inj (a b c:Set) (f:a->b)(f':b->c): injectiveC f-> injectiveC f' -> injectiveC (f' \o f).
proof: Proof. by move=> fi fi' x y p; apply: fi; apply: fi'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)