proposition: Lemma compose_surjective : forall x y z f g, Transformation.surjective x y f -> Transformation.surjective y z g -> Transformation.surjective x z (fun y=> g (f y)).
proof: Proof. ir; uhg; dj. apply Transformation.compose_axioms with y; try lu. uhg; ir. uh H; uh H0; ee. nin (H3 x0). ee. nin (H4 x1); ee. sh x2; ee; try am. rw H8. am. am. am. Qed.
imports: set_theory