proposition: Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z.
proof: Proof. Proof with auto. intros A ? x y z H H0 H1. assert(z == y) by (symmetry ; auto). assert(x == y) by (transitivity z ; eauto). contradiction. Qed.
imports: Coq.Program.Program Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms