proposition: Theorem ordered : order A le.
proof: Proof. split. unfold reflexive in |- *; intros. unfold le in |- *. case x. exact M1.le_refl. exact M2.le_refl. unfold le in |- *. unfold transitive in |- *. simple destruct x; simple destruct y; simple destruct z. intros; eapply M1.le_trans; eauto. auto. contradiction. auto. auto. contradiction. auto. intros; eapply M2.le_trans; eauto. unfold antisymmetric, A, le in |- *. simple destruct x; simple destruct y. intros a0 H0 H1; rewrite (M1.le_antisym _ _ H0 H1). trivial. contradiction. contradiction. intros a0 H0 H1; rewrite (M2.le_antisym _ _ H0 H1). trivial. Qed.
imports: Relations List ZArith