proposition: Lemma compare_ok_1: forall a a', (compare a a' = Datatypes.Lt <-> a < a') /\ (compare a a' = Datatypes.Eq <-> a = a') .
proof: Proof. induction a;simpl. destruct a';simpl. split;split. discriminate 1. inversion 1. auto. auto. split;split. auto with T1. auto. discriminate 1. discriminate 1. destruct a'; simpl. split; split. discriminate 1. inversion 1. inversion 1. discriminate 1. caseEq (compare a1 a'1). intros. case (lt_eq_lt_dec n n0). destruct s. repeat split. replace a1 with a'1. constructor 3;auto. case (IHa1 a'1). intros. case H1;auto. intros;symmetry. auto. discriminate 1. injection 1. intros; subst n0. absurd (n<n)%nat;auto with arith. split. repeat split. intro. subst n0. replace a1 with a'1. constructor 4. case (IHa2 a'2);intros. auto. case H1;auto. elim (IHa1 a'1);intros. case H2;auto. symmetry;auto. subst n0. replace a1 with a'1. intro. assert (lt a2 a'2). eapply lt_inv_b;eauto. case (IHa2 a'2);intros. case H2;auto. case (IHa1 a'1);intros. case H1;auto. intros;symmetry;auto. replace a1 with a'1. subst n0. repeat split. intros. case (IHa2 a'2); intros. replace a2 with a'2. auto. case H2;intros. symmetry;auto. injection 1. intro;subst a'2. case (IHa2 a2). intros. case H2;auto. case (IHa1 a'1);intros. case H1;intros;symmetry;auto. intro;repeat split. discriminate 1. intro H0. absurd (cons a1 n a2 < cons a'1 n0 a'2);auto. apply lt_not_gt. replace a1 with a'1. constructor 3;auto. elim (IHa1 a'1);intros. case H2;auto. symmetry;auto. discriminate 1. injection 1. intros; subst n0; absurd (n<n)%nat;auto with arith. intros; repeat split. constructor 2. case (IHa1 a'1);intros. case H1;auto. discriminate 1. injection 1;intros. subst a'1;absurd (lt a1 a1). apply lt_irr. case (IHa1 a1);intros. case H3;auto. intro;repeat split. discriminate 1. inversion 1. case (IHa1 a'1);intros. case H8;intros. rewrite <- (H11 H2). symmetry;auto. absurd (cons a'1 n0 a'2 < cons a1 n a2). apply lt_not_gt;auto. case (IHa1 a'1);intros. case H9;intros. rewrite H in H11. generalize (H11 H5). discriminate 1. case (IHa1 a'1);intros. case H9;intros. rewrite H in H11. generalize (H11 H5). discriminate 1. discriminate 1. injection 1;intros. subst a'1; case (IHa1 a1);intros. case H4;intros. rewrite H in H6. auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List