proposition: Lemma surj_set_quo_surjective : forall (E : Setoid) (R : Relation E) (p : equivalence R), surjective (surj_set_quo E R p).
proof: Proof. intros E R p; try assumption. red in |- *. intros y; exists y; try assumption. simpl in |- *. elim p. intros H'; red in H'. unfold app_rel in H'. auto with algebra. Qed.