proposition: Theorem ordered : order A le.
proof: Proof. split. unfold reflexive in |- *; intros. unfold le in |- *; case x. right. split; [ trivial | apply M2.le_refl; auto ]. unfold le, transitive in |- *. simple destruct x; simple destruct y; simple destruct z. simple destruct 1; intro H1. simple destruct 1. left. eapply M1.lt_trans. eexact H1. assumption. simple destruct 1. simple destruct 1. auto. simple destruct 1. intro. case H1; intros e H3; rewrite e; auto. case H1; intros e H3; rewrite e; auto. simple destruct 1. simple destruct 1. right. split; try auto. eapply M2.le_trans; eauto. unfold antisymmetric, A, le in |- *. simple destruct x; simple destruct y. simple destruct 1; simple destruct 2. intro. absurd (D1.lt a1 a1). apply M1.lt_irreflexive. eapply M1.lt_trans; eauto. simple destruct 1; intros e H3. rewrite e in H0. case (M1.lt_irreflexive a H0). case H0; intros e H3. rewrite e; intro H2. case (M1.lt_irreflexive a1 H2). simple destruct 1; intros e H3; rewrite e. case (M2.le_antisym a2 a0). auto. case H0; auto. auto. Qed.
imports: Relations List ZArith