proposition: Lemma Eq_Nat_equiv : Equivalence Eq_Nat.
proof: Proof. apply Build_Equivalence; unfold Eq_Nat in |- *. auto. apply Build_Partial_equivalence. unfold Transitive in |- *; intros x y z H1 H2; apply (trans_eq H1 H2). unfold Symmetric in |- *; intros x y H1; apply (sym_eq H1). Qed.
imports: Relations