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