proposition: Lemma inverse_image_of_eq : forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
proof: Proof. intros A B f; split; red; [ reflexivity | intros x y z; transitivity (f y); assumption | intros; symmetry ; assumption ]. Qed.
imports: Relation_Definitions Relation_Operators Operators_Properties