proposition: Lemma projected_strong_setoid `{StrongSetoid B} `{Equiv A} `{Apart A} (f: A → B) (eq_correct : ∀ x y, x = y ↔ f x = f y) (apart_correct : ∀ x y, x ≶ y ↔ f x ≶ f y) : StrongSetoid A.
proof: Proof. split. intros x. red. rewrite apart_correct. apply (irreflexivity (≶)). intros x y. rewrite !apart_correct. now symmetry. intros x y E z. rewrite !apart_correct. apply cotransitive. now apply apart_correct. intros x y. rewrite apart_correct, eq_correct. now apply tight_apart. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.jections