proposition: Lemma surjective_compose {X Y Z : Type} (f : X -> Y) (g : Y -> Z) : surjective f -> surjective g -> surjective (compose g f).
proof: Proof. intros. red; intros z. specialize (H0 z) as [y]. specialize (H y) as [x]. exists x. subst. reflexivity. Qed.
imports: Coq(Description) Coq(FunctionalExtensionality)