proposition: Lemma eq_sym : forall x y : t, eq x y -> eq y x.
proof: Proof. intros (x1,x2) (y1,y2); unfold eq; simpl; intuition auto with relations. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec