proposition: Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
proof: Proof. hnf. intros x y H0. red in H0. apply symmetry. assumption. Qed.
imports: Coq.Classes.Init Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions