proposition: Theorem ordered : order A le.
proof: Proof. split. - intro x; unfold le; case x. + exact M1.le_refl. + exact M2.le_refl. - intros x y z H H0. destruct x, y, z;eauto. + eapply M1.le_trans; eauto. + contradiction. + contradiction. + eapply M2.le_trans;eauto. - intros x y H H0; unfold le in |- *. destruct x, y. + now rewrite (M1.le_antisym _ _ H H0). + contradiction. + contradiction. + now rewrite (M2.le_antisym _ _ H H0). Qed.
imports: Relations List ZArith