proposition: Lemma composeC_bij (a b c:Set) (f:a->b)(f':b->c): bijectiveC f -> bijectiveC f' -> bijectiveC (f' \o f).
proof: Proof. move=> [fi fs] [fi' fs']. by split; [apply: composeC_inj| apply: composeC_surj ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)