proposition: Lemma proper_sym_flip : forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f), Proper (R1==>flip R2) f.
proof: Proof. intros A R1 Sym B R2 f Hf. intros x x' Hxx'. apply Hf, Sym, Hxx'. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses