proposition: Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
proof: Proof. firstorder. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses