proposition: Lemma classes_neq_related@{} : forall q r, ' q <> ' r -> ~ (equiv q r).
proof: Proof. intros q r E1 E2;apply E1,path,E2. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields