proposition: Lemma Surjections_compose : Surjective _ _ f -> Surjective _ _ g -> Surjective _ _ (f o g).
proof: Proof. unfold Surjective, comp in |- *; intros Sf Sg z. elim (Sg z); intros y E; elim (Sf y); intros x E'. exists x; rewrite E; rewrite E'; trivial. Qed.