proposition: Lemma projected_setoid `{Setoid B} `{Equiv A} (f : A → B) (eq_correct : ∀ x y, x = y ↔ f x = f y) : Setoid A.
proof: Proof. constructor; repeat intro; apply eq_correct. reflexivity. symmetry; now apply eq_correct. transitivity (f y); now apply eq_correct. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.products