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