proposition: Lemma comp_is_id_then_surjective : forall (A B : Setoid) (f : MAP A B) (g : MAP B A), Equal (comp_map_map f g) (Id B) -> surjective f.
proof: Proof. intros A B f g H'; try assumption. apply comp_surjective with B g; auto with algebra. apply surjective_comp with (f := Id B); auto with algebra. Qed.