proposition: Theorem ordered : order A le.
proof: Proof. split. - intro l; induction l as [ | a l' Il'] ; cbn; auto. - intros l1 ; induction l1; intros l2 l3; destruct l2,l3; cbn; auto. + contradiction. + intuition. * left; eapply M.lt_trans; eauto. * subst a1; auto. * subst a0; auto. * subst a0; right; split; [auto | eauto]. - intros l1; induction l1; intro l2; destruct l2. + reflexivity. + inversion 2. + inversion 1. + inversion 1. * inversion 1. absurd (D.lt a0 a0). apply M.lt_irreflexive. eapply M.lt_trans;eauto. destruct H2 as [H2 H3];subst a0. destruct (M.lt_irreflexive _ H0). * destruct H0 as [H0 H1]. subst a0; inversion_clear 1. destruct (M.lt_irreflexive _ H2). destruct H2 as [_ H3]. rewrite (IHl1 l2);auto. Qed.
imports: DecOrders