From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- lib/Coqlib.v | 178 +++++++++++++++++++++++++++++------------------------------ 1 file changed, 89 insertions(+), 89 deletions(-) (limited to 'lib/Coqlib.v') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 35d53854..4ec19fa9 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -107,14 +107,14 @@ Proof. intros. case (peq x y); intros. elim H; auto. auto. -Qed. +Qed. Definition Plt: positive -> positive -> Prop := Pos.lt. Lemma Plt_ne: forall (x y: positive), Plt x y -> x <> y. Proof. - unfold Plt; intros. red; intro. subst y. eelim Pos.lt_irrefl; eauto. + unfold Plt; intros. red; intro. subst y. eelim Pos.lt_irrefl; eauto. Qed. Hint Resolve Plt_ne: coqlib. @@ -125,7 +125,7 @@ Proof (Pos.lt_trans). Lemma Plt_succ: forall (x: positive), Plt x (Psucc x). Proof. - unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl. + unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl. Qed. Hint Resolve Plt_succ: coqlib. @@ -139,7 +139,7 @@ Hint Resolve Plt_succ: coqlib. Lemma Plt_succ_inv: forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y. Proof. - unfold Plt; intros. rewrite Pos.lt_succ_r in H. + unfold Plt; intros. rewrite Pos.lt_succ_r in H. apply Pos.le_lteq; auto. Qed. @@ -242,11 +242,11 @@ Lemma positive_Peano_ind: Proof. intros. apply (well_founded_ind Plt_wf P). - intros. + intros. case (peq x0 xH); intro. subst x0; auto. elim (Psucc_pred x0); intro. contradiction. rewrite <- H2. - apply H0. apply H1. apply Ppred_Plt. auto. + apply H0. apply H1. apply Ppred_Plt. auto. Qed. End POSITIVE_ITERATION. @@ -269,14 +269,14 @@ Proof. intros. case (zeq x y); intros. elim H; auto. auto. -Qed. +Qed. Open Scope Z_scope. Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_dec. Lemma zlt_true: - forall (A: Type) (x y: Z) (a b: A), + forall (A: Type) (x y: Z) (a b: A), x < y -> (if zlt x y then a else b) = a. Proof. intros. case (zlt x y); intros. @@ -285,7 +285,7 @@ Proof. Qed. Lemma zlt_false: - forall (A: Type) (x y: Z) (a b: A), + forall (A: Type) (x y: Z) (a b: A), x >= y -> (if zlt x y then a else b) = b. Proof. intros. case (zlt x y); intros. @@ -296,7 +296,7 @@ Qed. Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec. Lemma zle_true: - forall (A: Type) (x y: Z) (a b: A), + forall (A: Type) (x y: Z) (a b: A), x <= y -> (if zle x y then a else b) = a. Proof. intros. case (zle x y); intros. @@ -305,7 +305,7 @@ Proof. Qed. Lemma zle_false: - forall (A: Type) (x y: Z) (a b: A), + forall (A: Type) (x y: Z) (a b: A), x > y -> (if zle x y then a else b) = b. Proof. intros. case (zle x y); intros. @@ -327,7 +327,7 @@ Qed. Lemma two_power_nat_two_p: forall x, two_power_nat x = two_p (Z_of_nat x). Proof. - induction x. auto. + induction x. auto. rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega. Qed. @@ -335,7 +335,7 @@ Lemma two_p_monotone: forall x y, 0 <= x <= y -> two_p x <= two_p y. Proof. intros. - replace (two_p x) with (two_p x * 1) by omega. + replace (two_p x) with (two_p x * 1) by omega. replace y with (x + (y - x)) by omega. rewrite two_p_is_exp; try omega. apply Zmult_le_compat_l. @@ -356,7 +356,7 @@ Lemma two_p_strict: Proof. intros x0 GT. pattern x0. apply natlike_ind. simpl. omega. - intros. rewrite two_p_S; auto. generalize (two_p_gt_ZERO x H). omega. + intros. rewrite two_p_S; auto. generalize (two_p_gt_ZERO x H). omega. omega. Qed. @@ -366,7 +366,7 @@ Proof. intros. assert (x = 0 \/ x - 1 >= 0) by omega. destruct H0. subst. vm_compute. auto. replace (two_p x) with (2 * two_p (x - 1)). - generalize (two_p_strict _ H0). omega. + generalize (two_p_strict _ H0). omega. rewrite <- two_p_S. decEq. omega. omega. Qed. @@ -377,7 +377,7 @@ Lemma Zmin_spec: Proof. intros. case (zlt x y); unfold Zlt, Zge; intro z. unfold Zmin. rewrite z. auto. - unfold Zmin. caseEq (x ?= y); intro. + unfold Zmin. caseEq (x ?= y); intro. apply Zcompare_Eq_eq. auto. contradiction. reflexivity. @@ -411,21 +411,21 @@ Qed. Lemma Zdiv_small: forall x y, 0 <= x < y -> x / y = 0. Proof. - intros. assert (y > 0). omega. + intros. assert (y > 0). omega. assert (forall a b, 0 <= a < y -> 0 <= y * b + a < y -> b = 0). - intros. + intros. assert (b = 0 \/ b > 0 \/ (-b) > 0). omega. elim H3; intro. auto. elim H4; intro. - assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega. - omegaContradiction. + assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega. + omegaContradiction. assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega. rewrite <- Zopp_mult_distr_r in H6. omegaContradiction. - apply H1 with (x mod y). + apply H1 with (x mod y). apply Z_mod_lt. auto. rewrite <- Z_div_mod_eq. auto. auto. Qed. @@ -434,7 +434,7 @@ Lemma Zmod_small: forall x y, 0 <= x < y -> x mod y = x. Proof. intros. assert (y > 0). omega. - generalize (Z_div_mod_eq x y H0). + generalize (Z_div_mod_eq x y H0). rewrite (Zdiv_small x y H). omega. Qed. @@ -442,7 +442,7 @@ Lemma Zmod_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x mod y = b. Proof. - intros. subst x. rewrite Zplus_comm. + intros. subst x. rewrite Zplus_comm. rewrite Z_mod_plus. apply Zmod_small. auto. omega. Qed. @@ -463,12 +463,12 @@ Proof. generalize (Z_div_mod_eq (a/b) c H0). generalize (Z_mod_lt (a/b) c H0). intros. set (q1 := a / b) in *. set (r1 := a mod b) in *. set (q2 := q1 / c) in *. set (r2 := q1 mod c) in *. - symmetry. apply Zdiv_unique with (r2 * b + r1). + symmetry. apply Zdiv_unique with (r2 * b + r1). rewrite H2. rewrite H4. ring. - split. + split. assert (0 <= r2 * b). apply Zmult_le_0_compat. omega. omega. omega. assert ((r2 + 1) * b <= c * b). - apply Zmult_le_compat_r. omega. omega. + apply Zmult_le_compat_r. omega. omega. replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring. replace (c * b) with (b * c) in H5 by ring. omega. @@ -490,17 +490,17 @@ Lemma Zdiv_interval_1: lo * b <= a < hi * b -> lo <= a/b < hi. Proof. - intros. + intros. generalize (Z_div_mod_eq a b H1). generalize (Z_mod_lt a b H1). intros. set (q := a/b) in *. set (r := a mod b) in *. split. assert (lo < (q + 1)). - apply Zmult_lt_reg_r with b. omega. - apply Zle_lt_trans with a. omega. + apply Zmult_lt_reg_r with b. omega. + apply Zle_lt_trans with a. omega. replace ((q + 1) * b) with (b * q + b) by ring. omega. omega. - apply Zmult_lt_reg_r with b. omega. + apply Zmult_lt_reg_r with b. omega. replace (q * b) with (b * q) by ring. omega. Qed. @@ -513,7 +513,7 @@ Proof. intros. assert (lo <= a / b < hi+1). apply Zdiv_interval_1. omega. omega. auto. - assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega. + assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega. replace (lo * 1) with lo in H3 by ring. assert ((hi + 1) * 1 <= (hi + 1) * b). apply Zmult_le_compat_l. omega. omega. replace ((hi + 1) * 1) with (hi + 1) in H4 by ring. @@ -526,19 +526,19 @@ Lemma Zmod_recombine: a > 0 -> b > 0 -> x mod (a * b) = ((x/b) mod a) * b + (x mod b). Proof. - intros. - set (xb := x/b). + intros. + set (xb := x/b). apply Zmod_unique with (xb/a). generalize (Z_div_mod_eq x b H0); fold xb; intro EQ1. generalize (Z_div_mod_eq xb a H); intro EQ2. - rewrite EQ2 in EQ1. + rewrite EQ2 in EQ1. eapply trans_eq. eexact EQ1. ring. - generalize (Z_mod_lt x b H0). intro. + generalize (Z_mod_lt x b H0). intro. generalize (Z_mod_lt xb a H). intro. assert (0 <= xb mod a * b <= a * b - b). split. apply Zmult_le_0_compat; omega. replace (a * b - b) with ((a - 1) * b) by ring. - apply Zmult_le_compat; omega. + apply Zmult_le_compat; omega. omega. Qed. @@ -554,10 +554,10 @@ Definition Zdivide_dec: forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }. Proof. intros. destruct (zeq (Zmod q p) 0). - left. exists (q / p). + left. exists (q / p). transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto. transitivity (p * (q / p)). omega. ring. - right; red; intros. elim n. apply Z_div_exact_1; auto. + right; red; intros. elim n. apply Z_div_exact_1; auto. inv H0. rewrite Z_div_mult; auto. ring. Defined. Global Opaque Zdivide_dec. @@ -567,7 +567,7 @@ Lemma Zdivide_interval: 0 < c -> 0 <= a < b -> (c | a) -> (c | b) -> 0 <= a <= b - c. Proof. intros. destruct H1 as [x EQ1]. destruct H2 as [y EQ2]. subst. destruct H0. - split. omega. exploit Zmult_lt_reg_r; eauto. intros. + split. omega. exploit Zmult_lt_reg_r; eauto. intros. replace (y * c - c) with ((y - 1) * c) by ring. apply Zmult_le_compat_r; omega. Qed. @@ -585,9 +585,9 @@ Qed. Lemma nat_of_Z_max: forall z, Z_of_nat (nat_of_Z z) = Zmax z 0. Proof. - intros. unfold Zmax. destruct z; simpl; auto. + intros. unfold Zmax. destruct z; simpl; auto. change (Z.of_nat (Z.to_nat (Zpos p)) = Zpos p). - apply Z2Nat.id. compute; intuition congruence. + apply Z2Nat.id. compute; intuition congruence. Qed. Lemma nat_of_Z_eq: @@ -607,7 +607,7 @@ Lemma nat_of_Z_plus: p >= 0 -> q >= 0 -> nat_of_Z (p + q) = (nat_of_Z p + nat_of_Z q)%nat. Proof. - unfold nat_of_Z; intros. apply Z2Nat.inj_add; omega. + unfold nat_of_Z; intros. apply Z2Nat.inj_add; omega. Qed. @@ -619,9 +619,9 @@ Definition align (n: Z) (amount: Z) := Lemma align_le: forall x y, y > 0 -> x <= align x y. Proof. - intros. unfold align. + intros. unfold align. generalize (Z_div_mod_eq (x + y - 1) y H). intro. - replace ((x + y - 1) / y * y) + replace ((x + y - 1) / y * y) with ((x + y - 1) - (x + y - 1) mod y). generalize (Z_mod_lt (x + y - 1) y H). omega. rewrite Zmult_comm. omega. @@ -629,7 +629,7 @@ Qed. Lemma align_divides: forall x y, y > 0 -> (y | align x y). Proof. - intros. unfold align. apply Zdivide_factor_l. + intros. unfold align. apply Zdivide_factor_l. Qed. (** * Definitions and theorems on the data types [option], [sum] and [list] *) @@ -709,14 +709,14 @@ Lemma list_length_z_cons: list_length_z (hd :: tl) = list_length_z tl + 1. Proof. intros. unfold list_length_z. simpl. - rewrite (list_length_z_aux_shift tl 1 0). omega. + rewrite (list_length_z_aux_shift tl 1 0). omega. Qed. Lemma list_length_z_pos: forall (A: Type) (l: list A), list_length_z l >= 0. Proof. - induction l; simpl. unfold list_length_z; simpl. omega. + induction l; simpl. unfold list_length_z; simpl. omega. rewrite list_length_z_cons. omega. Qed. @@ -725,7 +725,7 @@ Lemma list_length_z_map: list_length_z (map f l) = list_length_z l. Proof. induction l. reflexivity. simpl. repeat rewrite list_length_z_cons. congruence. -Qed. +Qed. (** Extract the n-th element of a list, as [List.nth_error] does, but the index [n] is of type [Z]. *) @@ -740,7 +740,7 @@ Lemma list_nth_z_in: forall (A: Type) (l: list A) n x, list_nth_z l n = Some x -> In x l. Proof. - induction l; simpl; intros. + induction l; simpl; intros. congruence. destruct (zeq n 0). left; congruence. right; eauto. Qed. @@ -762,7 +762,7 @@ Proof. discriminate. rewrite list_length_z_cons. destruct (zeq n 0). generalize (list_length_z_pos l); omega. - exploit IHl; eauto. unfold Zpred. omega. + exploit IHl; eauto. unfold Zpred. omega. Qed. (** Properties of [List.incl] (list inclusion). *) @@ -795,7 +795,7 @@ Lemma incl_same_head: forall (A: Type) (x: A) (l1 l2: list A), incl l1 l2 -> incl (x::l1) (x::l2). Proof. - intros; red; simpl; intros. intuition. + intros; red; simpl; intros. intuition. Qed. (** Properties of [List.map] (mapping a function over a list). *) @@ -848,9 +848,9 @@ Lemma list_in_map_inv: Proof. induction l; simpl; intros. contradiction. - elim H; intro. + elim H; intro. exists a; intuition auto. - generalize (IHl y H0). intros [x [EQ IN]]. + generalize (IHl y H0). intros [x [EQ IN]]. exists x; tauto. Qed. @@ -869,8 +869,8 @@ Lemma list_append_map_inv: Proof. induction m1; simpl; intros. exists (@nil A); exists l; auto. - destruct l; simpl in H; inv H. - exploit IHm1; eauto. intros [l1 [l2 [P [Q R]]]]. subst l. + destruct l; simpl in H; inv H. + exploit IHm1; eauto. intros [l1 [l2 [P [Q R]]]]. subst l. exists (a0 :: l1); exists l2; intuition. simpl; congruence. Qed. @@ -897,7 +897,7 @@ Remark list_fold_left_app: forall l1 l2 accu, list_fold_left accu (l1 ++ l2) = list_fold_left (list_fold_left accu l1) l2. Proof. - induction l1; simpl; intros. + induction l1; simpl; intros. auto. rewrite IHl1. auto. Qed. @@ -907,11 +907,11 @@ Lemma list_fold_right_eq: list_fold_right l base = match l with nil => base | x :: l' => f x (list_fold_right l' base) end. Proof. - unfold list_fold_right; intros. + unfold list_fold_right; intros. destruct l. auto. - unfold rev'. rewrite <- ! rev_alt. simpl. - rewrite list_fold_left_app. simpl. auto. + unfold rev'. rewrite <- ! rev_alt. simpl. + rewrite list_fold_left_app. simpl. auto. Qed. Lemma list_fold_right_spec: @@ -943,7 +943,7 @@ Proof. intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto. Qed. -(** [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements +(** [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements in common. *) Definition list_disjoint (A: Type) (l1 l2: list A) : Prop := @@ -967,21 +967,21 @@ Lemma list_disjoint_cons_left: forall (A: Type) (a: A) (l1 l2: list A), list_disjoint (a :: l1) l2 -> list_disjoint l1 l2. Proof. - unfold list_disjoint; simpl; intros. apply H; tauto. + unfold list_disjoint; simpl; intros. apply H; tauto. Qed. Lemma list_disjoint_cons_right: forall (A: Type) (a: A) (l1 l2: list A), list_disjoint l1 (a :: l2) -> list_disjoint l1 l2. Proof. - unfold list_disjoint; simpl; intros. apply H; tauto. + unfold list_disjoint; simpl; intros. apply H; tauto. Qed. Lemma list_disjoint_notin: forall (A: Type) (l1 l2: list A) (a: A), list_disjoint l1 l2 -> In a l1 -> ~(In a l2). Proof. - unfold list_disjoint; intros; red; intros. + unfold list_disjoint; intros; red; intros. apply H with a a; auto. Qed. @@ -989,7 +989,7 @@ Lemma list_disjoint_sym: forall (A: Type) (l1 l2: list A), list_disjoint l1 l2 -> list_disjoint l2 l1. Proof. - unfold list_disjoint; intros. + unfold list_disjoint; intros. apply sym_not_equal. apply H; auto. Qed. @@ -1000,9 +1000,9 @@ Proof. induction l1; intros. left; red; intros. elim H. case (In_dec eqA_dec a l2); intro. - right; red; intro. apply (H a a); auto with coqlib. + right; red; intro. apply (H a a); auto with coqlib. case (IHl1 l2); intro. - left; red; intros. elim H; intro. + left; red; intros. elim H; intro. red; intro; subst a y. contradiction. apply l; auto. right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto. @@ -1029,9 +1029,9 @@ Lemma list_norepet_dec: Proof. induction l. left; constructor. - destruct IHl. + destruct IHl. case (In_dec eqA_dec a l); intro. - right. red; intro. inversion H. contradiction. + right. red; intro. inversion H. contradiction. left. constructor; auto. right. red; intro. inversion H. contradiction. Defined. @@ -1047,7 +1047,7 @@ Proof. constructor. red; intro. generalize (list_in_map_inv f _ _ H2). intros [x [EQ IN]]. generalize EQ. change (f hd <> f x). - apply H1. tauto. tauto. + apply H1. tauto. tauto. red; intro; subst x. contradiction. apply IHlist_norepet. intros. apply H1. tauto. tauto. auto. Qed. @@ -1057,20 +1057,20 @@ Remark list_norepet_append_commut: list_norepet (a ++ b) -> list_norepet (b ++ a). Proof. intro A. - assert (forall (x: A) (b: list A) (a: list A), - list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) -> + assert (forall (x: A) (b: list A) (a: list A), + list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) -> list_norepet (a ++ x :: b)). induction a; simpl; intros. constructor; auto. inversion H. constructor. red; intro. elim (in_app_or _ _ _ H6); intro. elim H4. apply in_or_app. tauto. - elim H7; intro. subst a. elim H0. left. auto. + elim H7; intro. subst a. elim H0. left. auto. elim H4. apply in_or_app. tauto. auto. induction a; simpl; intros. rewrite <- app_nil_end. auto. - inversion H0. apply H. auto. + inversion H0. apply H. auto. red; intro; elim H3. apply in_or_app. tauto. red; intro; elim H3. apply in_or_app. tauto. Qed. @@ -1085,10 +1085,10 @@ Proof. tauto. inversion H; subst. rewrite IHl1 in H3. rewrite in_app in H2. intuition. - constructor; auto. red; intros. elim H2; intro. congruence. auto. - destruct H as [B [C D]]. inversion B; subst. - constructor. rewrite in_app. intuition. elim (D a a); auto. apply in_eq. - rewrite IHl1. intuition. red; intros. apply D; auto. apply in_cons; auto. + constructor; auto. red; intros. elim H2; intro. congruence. auto. + destruct H as [B [C D]]. inversion B; subst. + constructor. rewrite in_app. intuition. elim (D a a); auto. apply in_eq. + rewrite IHl1. intuition. red; intros. apply D; auto. apply in_cons; auto. Qed. Lemma list_norepet_append: @@ -1133,7 +1133,7 @@ Lemma is_tail_cons_left: forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2. Proof. induction c2; intros; inversion H. - constructor. constructor. constructor. auto. + constructor. constructor. constructor. auto. Qed. Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib. @@ -1171,10 +1171,10 @@ Inductive list_forall2: list A -> list B -> Prop := Lemma list_forall2_app: forall a2 b2 a1 b1, - list_forall2 a1 b1 -> list_forall2 a2 b2 -> + list_forall2 a1 b1 -> list_forall2 a2 b2 -> list_forall2 (a1 ++ a2) (b1 ++ b2). Proof. - induction 1; intros; simpl. auto. constructor; auto. + induction 1; intros; simpl. auto. constructor; auto. Qed. Lemma list_forall2_length: @@ -1195,7 +1195,7 @@ Lemma list_forall2_imply: Proof. induction 1; intros. constructor. - constructor. auto with coqlib. apply IHlist_forall2; auto. + constructor. auto with coqlib. apply IHlist_forall2; auto. intros. auto with coqlib. Qed. @@ -1210,7 +1210,7 @@ Fixpoint list_drop (A: Type) (n: nat) (x: list A) {struct n} : list A := Lemma list_drop_incl: forall (A: Type) (x: A) n (l: list A), In x (list_drop n l) -> In x l. Proof. - induction n; simpl; intros. auto. + induction n; simpl; intros. auto. destruct l; auto with coqlib. Qed. @@ -1225,7 +1225,7 @@ Lemma list_map_drop: forall (A B: Type) (f: A -> B) n (l: list A), list_drop n (map f l) = map f (list_drop n l). Proof. - induction n; simpl; intros. auto. + induction n; simpl; intros. auto. destruct l; simpl; auto. Qed. @@ -1267,7 +1267,7 @@ Qed. Lemma proj_sumbool_is_true: forall (P: Prop) (a: {P}+{~P}), P -> proj_sumbool a = true. Proof. - intros. unfold proj_sumbool. destruct a. auto. contradiction. + intros. unfold proj_sumbool. destruct a. auto. contradiction. Qed. Ltac InvBooleans := @@ -1306,7 +1306,7 @@ Lemma dec_eq_sym: (if dec_eq x y then ifso else ifnot) = (if dec_eq y x then ifso else ifnot). Proof. - intros. destruct (dec_eq x y). + intros. destruct (dec_eq x y). subst y. rewrite dec_eq_true. auto. rewrite dec_eq_false; auto. Qed. @@ -1352,22 +1352,22 @@ Inductive lex_ord: A*B -> A*B -> Prop := | lex_ord_right: forall a b1 b2, ordB b1 b2 -> lex_ord (a,b1) (a,b2). -Lemma wf_lex_ord: +Lemma wf_lex_ord: well_founded ordA -> well_founded ordB -> well_founded lex_ord. Proof. intros Awf Bwf. assert (forall a, Acc ordA a -> forall b, Acc ordB b -> Acc lex_ord (a, b)). induction 1. induction 1. constructor; intros. inv H3. apply H0. auto. apply Bwf. - apply H2; auto. + apply H2; auto. red; intros. destruct a as [a b]. apply H; auto. Qed. Lemma transitive_lex_ord: transitive _ ordA -> transitive _ ordB -> transitive _ lex_ord. Proof. - intros trA trB; red; intros. - inv H; inv H0. + intros trA trB; red; intros. + inv H; inv H0. left; eapply trA; eauto. left; auto. left; auto. -- cgit