proposition: Lemma inverse_image_of_equivalence : forall (A B:Type) (f:A -> B) (r:relation B), equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
proof: Proof. intros A B f r H; split; elim H; red; auto. intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. Qed.
imports: Relation_Definitions Relation_Operators Operators_Properties