proposition: Theorem ordered : order A le.
proof: Proof. split. - unfold le ; intro x; case x. right;split; [ trivial | apply M2.le_refl; auto ]. - intros x y z; destruct x,y,z,1. + destruct 1. * left; eapply M1.lt_trans;eauto. * destruct H0; subst a3; now left. + destruct H; subst a1; destruct 1. * now left. * destruct H; subst a3; right; split. reflexivity. eapply M2.le_trans; eauto. - intros x y H H0; destruct x, y,H,H0. absurd (D1.lt a1 a1). + apply M1.lt_irreflexive. + eapply M1.lt_trans; eauto. + destruct H0; subst a1. case (M1.lt_irreflexive a H). + destruct H; subst a1; case (M1.lt_irreflexive _ H0). + destruct H,H0; subst a1; rewrite (M2.le_antisym a0 a2);auto. Qed.
imports: Relations List ZArith