proposition: Theorem ordered : order A le.
proof: Proof. split. unfold A, le, reflexive in |- *. intro x; case x; simpl in |- *; auto. unfold A, le, transitive in |- *; simple destruct x; simple destruct y; auto; simple destruct z; auto. unfold A, le, antisymmetric in |- *; simple destruct x; simple destruct y; simpl in |- *; auto; contradiction. Qed.
imports: Relations List ZArith Arith