proposition: Theorem ordered : order A le.
proof: Proof. split. unfold A, le, reflexive in |- *; auto with arith. unfold A, le, transitive in |- *; eauto with arith. unfold A, le, antisymmetric in |- *; eauto with arith. Qed.
imports: Relations List ZArith Arith