proposition: Lemma comp_surjective : forall (A B C : Setoid) (f : MAP A B) (g : MAP B C), surjective (comp_map_map g f) -> surjective g.
proof: Proof. unfold surjective in |- *. intros A B C f g H' y; try assumption. elim (H' y); intros x E; try exact E. simpl in E. unfold comp_map_fun in E. exists (Ap f x); try assumption; auto with algebra. Qed.