proposition: Lemma c3f_fb u v: bijection u -> bijection v -> bijection (compose3function u v).
proof: Proof. move=> [iu su][iv sv]; split; first by apply: c3f_fi=>//. apply: c3f_fs=>//. case: (emptyset_dichot (target u)); first by right; right; right. move=> [y yt]; move: (surjective_pr su yt)=> [x xs _]; left; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)