From dc8858d764a6eb77d0d0dd15ed2e3abc55b717cf Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 22 Oct 2015 16:09:26 -0400 Subject: [PATCH] refactor(library/init/nat,library/): protect more nat theorems --- library/algebra/order.lean | 3 ++ library/data/finset/card.lean | 2 +- library/data/int/basic.lean | 8 ++--- library/data/nat/basic.lean | 6 ++-- library/data/nat/bquant.lean | 4 +-- library/data/nat/div.lean | 2 +- library/data/nat/order.lean | 36 ++++++++++----------- library/data/nat/sub.lean | 4 +-- library/data/pnat.lean | 2 +- library/init/nat.lean | 60 +++++++++++++++++------------------ library/logic/weak_fan.lean | 2 +- 11 files changed, 65 insertions(+), 64 deletions(-) diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 489e38d4a2..2804d9bc8f 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -54,6 +54,9 @@ section theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl theorem not_lt_self (a : A) : ¬ a < a := !lt.irrefl -- alternate syntax + theorem lt_self_iff_false [simp] (a : A) : a < a ↔ false := + iff_false_intro (lt.irrefl a) + theorem lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans theorem gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1 diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean index e0ac2cc5fb..a30964e302 100644 --- a/library/data/finset/card.lean +++ b/library/data/finset/card.lean @@ -131,7 +131,7 @@ finset.induction_on s (assume Hnfa : f a ∉ image f s', have H2 : card (image f s') + 1 = card s' + 1, by rewrite [card_insert_of_not_mem Hnfa at H1]; assumption, - have H3 : card (image f s') = card s', from add.cancel_right H2, + have H3 : card (image f s') = card s', from add.right_cancel H2, have injf : inj_on f (ts s'), from IH H3, show inj_on f (set.insert a (ts s')), from take x1 x2, diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index c85a0a2b52..8b02cbd631 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -178,7 +178,7 @@ calc ... = pr2 q + pr1 p : by rewrite add.comm protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r := -add.cancel_right (calc +add.right_cancel (calc pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by rewrite add.right_comm ... = pr2 p + pr1 q + pr2 r : {H1} ... = pr2 p + (pr1 q + pr2 r) : by rewrite add.assoc @@ -221,7 +221,7 @@ theorem abstr_repr : Π (a : ℤ), abstr (repr a) = a | -[1+ m] := rfl theorem repr_sub_nat_nat (m n : ℕ) : repr (sub_nat_nat m n) ≡ (m, n) := -lt_ge_by_cases +nat.lt_ge_by_cases (take H : m < n, have H1 : repr (sub_nat_nat m n) = (0, n - m), by rewrite [sub_nat_nat_of_lt H, -(succ_pred_of_pos (sub_pos_of_lt H))], @@ -271,7 +271,7 @@ section local attribute abstr [reducible] local attribute dist [reducible] theorem nat_abs_abstr : Π (p : ℕ × ℕ), nat_abs (abstr p) = dist (pr1 p) (pr2 p) -| (m, n) := lt_ge_by_cases +| (m, n) := nat.lt_ge_by_cases (assume H : m < n, calc nat_abs (abstr (m, n)) = nat_abs (-[1+ pred (n - m)]) : int.abstr_of_lt H @@ -462,7 +462,7 @@ theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b) theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ} (H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm) : xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) := -nat.add.cancel_right (calc +nat.add.right_cancel (calc xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn)) = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : by rewrite add.comm4 ... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : by rewrite {xb*ym+yb*xm +_}nat.add_comm diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index d93101e7c4..32997d975f 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -151,7 +151,7 @@ left_comm nat.add_comm nat.add_assoc protected theorem add.right_comm : Π (n m k : ℕ), n + m + k = n + k + m := right_comm nat.add_comm nat.add_assoc -theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k := +protected theorem add.left_cancel {n m k : ℕ} : n + m = n + k → m = k := nat.induction_on n (take H : 0 + m = 0 + k, !nat.zero_add⁻¹ ⬝ H ⬝ !nat.zero_add) @@ -164,9 +164,9 @@ nat.induction_on n have n + m = n + k, from succ.inj this, IH this) -theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k := +protected theorem add.right_cancel {n m k : ℕ} (H : n + m = k + m) : n = k := have H2 : m + n = m + k, from !nat.add_comm ⬝ H ⬝ !nat.add_comm, - add.cancel_left H2 + add.left_cancel H2 theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 := nat.induction_on n diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index c86b6dac2e..470b60b4fb 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -54,7 +54,7 @@ namespace nat theorem not_bex_succ {P : nat → Prop} {n : nat} (H₁ : ¬ bex n P) (H₂ : ¬ P n) : ¬ bex (succ n) P := λ H, obtain (w : nat) (Hw : w < succ n ∧ P w), from H, - and.rec_on Hw (λ hltsn hp, or.rec_on (eq_or_lt_of_le (le_of_succ_le_succ hltsn)) + and.rec_on Hw (λ hltsn hp, or.rec_on (nat.eq_or_lt_of_le (le_of_succ_le_succ hltsn)) (λ heq : w = n, absurd (eq.rec_on heq hp) H₂) (λ hltn : w < n, absurd (exists.intro w (and.intro hltn hp)) H₁)) @@ -68,7 +68,7 @@ namespace nat λ x Hlt, H x (lt.step Hlt) theorem ball_succ_of_ball {n : nat} {P : nat → Prop} (H₁ : ball n P) (H₂ : P n) : ball (succ n) P := - λ (x : nat) (Hlt : x < succ n), or.elim (eq_or_lt_of_le (le_of_succ_le_succ Hlt)) + λ (x : nat) (Hlt : x < succ n), or.elim (nat.eq_or_lt_of_le (le_of_succ_le_succ Hlt)) (λ heq : x = n, eq.rec_on (eq.rec_on heq rfl) H₂) (λ hlt : x < n, H₁ x hlt) diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index cd147b56cf..64f3ea8acd 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -247,7 +247,7 @@ calc theorem eq_quotient {q1 r1 q2 r2 y : ℕ} (H1 : r1 < y) (H2 : r2 < y) (H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 := have H4 : q1 * y + r2 = q2 * y + r2, from (eq_remainder H1 H2 H3) ▸ H3, -have H5 : q1 * y = q2 * y, from add.cancel_right H4, +have H5 : q1 * y = q2 * y, from add.right_cancel H4, have H6 : y > 0, from lt_of_le_of_lt !zero_le H1, show q1 = q2, from eq_of_mul_eq_mul_right H6 H5 diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 79b4d31676..67004ebb9b 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -13,20 +13,20 @@ namespace nat /- lt and le -/ protected theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n := -le_of_eq_or_lt (or.swap H) +nat.le_of_eq_or_lt (or.swap H) protected theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n := -or.swap (eq_or_lt_of_le H) +or.swap (nat.eq_or_lt_of_le H) protected theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n := iff.intro nat.lt_or_eq_of_le nat.le_of_lt_or_eq protected theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) : m ≠ n → m < n := -or_resolve_right (eq_or_lt_of_le H1) +or_resolve_right (nat.eq_or_lt_of_le H1) protected theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n := iff.intro - (take H, and.intro (le_of_lt H) (take H1, !lt.irrefl (H1 ▸ H))) + (take H, and.intro (nat.le_of_lt H) (take H1, !lt.irrefl (H1 ▸ H))) (and.rec nat.lt_of_le_and_ne) theorem le_add_right (n k : ℕ) : n ≤ n + k := @@ -43,7 +43,7 @@ le.rec (exists.intro 0 rfl) (λm h, Exists.rec (λ k H, exists.intro (succ k) (H ▸ rfl))) protected theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m := -or.imp_left le_of_lt !lt_or_ge +or.imp_left nat.le_of_lt !nat.lt_or_ge /- addition -/ @@ -54,10 +54,10 @@ protected theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k !add.comm ▸ !add.comm ▸ nat.add_le_add_left H k protected theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m := -obtain l Hl, from le.elim H, le.intro (add.cancel_left (!add.assoc⁻¹ ⬝ Hl)) +obtain l Hl, from le.elim H, le.intro (add.left_cancel (!add.assoc⁻¹ ⬝ Hl)) protected theorem lt_of_add_lt_add_left {k n m : ℕ} (H : k + n < k + m) : n < m := -let H' := le_of_lt H in +let H' := nat.le_of_lt H in nat.lt_of_le_and_ne (nat.le_of_add_le_add_left H') (assume Heq, !lt.irrefl (Heq ▸ H)) protected theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m := @@ -83,7 +83,7 @@ protected theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * le.trans (!nat.mul_le_mul_right H1) (!nat.mul_le_mul_left H2) protected theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m := -lt_of_lt_of_le (nat.lt_add_of_pos_right Hk) (!mul_succ ▸ nat.mul_le_mul_left k (succ_le_of_lt H)) +nat.lt_of_lt_of_le (nat.lt_add_of_pos_right Hk) (!mul_succ ▸ nat.mul_le_mul_left k (succ_le_of_lt H)) protected theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k := !mul.comm ▸ !mul.comm ▸ nat.mul_lt_mul_of_pos_left H Hk @@ -95,19 +95,19 @@ open algebra protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] : algebra.decidable_linear_ordered_semiring nat := ⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring, - add_left_cancel := @add.cancel_left, - add_right_cancel := @add.cancel_right, + add_left_cancel := @nat.add.left_cancel, + add_right_cancel := @nat.add.right_cancel, lt := nat.lt, le := nat.le, - le_refl := le.refl, - le_trans := @le.trans, - le_antisymm := @le.antisymm, - le_total := @le.total, + le_refl := nat.le.refl, + le_trans := @nat.le.trans, + le_antisymm := @nat.le.antisymm, + le_total := @nat.le.total, le_iff_lt_or_eq := @nat.le_iff_lt_or_eq, - le_of_lt := @le_of_lt, - lt_irrefl := @lt.irrefl, - lt_of_lt_of_le := @lt_of_lt_of_le, - lt_of_le_of_lt := @lt_of_le_of_lt, + le_of_lt := @nat.le_of_lt, + lt_irrefl := @nat.lt.irrefl, + lt_of_lt_of_le := @nat.lt_of_lt_of_le, + lt_of_le_of_lt := @nat.lt_of_le_of_lt, lt_of_add_lt_add_left := @nat.lt_of_add_lt_add_left, add_lt_add_left := @nat.add_lt_add_left, add_le_add_left := @nat.add_le_add_left, diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 5ae9598380..9dd1078463 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -251,7 +251,7 @@ have H2 : k - n + n = m + n, from k - n + n = k : sub_add_cancel (le.intro H) ... = n + m : H⁻¹ ... = m + n : !add.comm, -add.cancel_right H2 +add.right_cancel H2 theorem eq_sub_of_add_eq {a b c : ℕ} (H : a + c = b) : a = b - c := (sub_eq_of_add_eq (!add.comm ▸ H))⁻¹ @@ -287,7 +287,7 @@ sub.cases ... = m + m' : Hl ... = k : Hm ... = k - n + n : sub_add_cancel H3, - le.intro (add.cancel_right H4)) + le.intro (add.right_cancel H4)) open algebra diff --git a/library/data/pnat.lean b/library/data/pnat.lean index f6b3f83ca4..0cafb48577 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -88,7 +88,7 @@ theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a := begin rewrite lt.def at H, exact pnat.eq (max_eq_left (le_of_not_gt H)) end theorem le_of_lt {a b : ℕ+} : a < b → a ≤ b := -begin rewrite [lt.def, le.def], apply le_of_lt end +begin rewrite [lt.def, le.def], apply nat.le_of_lt end theorem not_lt_of_ge {a b : ℕ+} : a ≤ b → ¬ (b < a) := begin rewrite [lt.def, le.def], apply not_lt_of_ge end diff --git a/library/init/nat.lean b/library/init/nat.lean index 28780b8bec..6cf2c82157 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -40,13 +40,13 @@ namespace nat /- basic definitions on natural numbers -/ inductive le (a : ℕ) : ℕ → Prop := - | refl : le a a + | refl' : le a a -- use refl' to avoid overloading le.refl | step : Π {b}, le a b → le a (succ b) definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le - lemma le_refl [refl] : ∀ a : nat, a ≤ a := - le.refl + protected lemma le.refl [refl] : ∀ a : nat, a ≤ a := + le.refl' protected definition lt [reducible] (n m : ℕ) := succ n ≤ m definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt @@ -85,7 +85,7 @@ namespace nat /- properties of inequality -/ - theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !le.refl + protected theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !le.refl theorem le_succ (n : ℕ) : n ≤ succ n := le.step !le.refl @@ -97,14 +97,14 @@ namespace nat theorem pred_le_iff_true [simp] (n : ℕ) : pred n ≤ n ↔ true := iff_true_intro (pred_le n) - theorem le.trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k := + protected theorem le.trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k := le.rec H1 (λp H2, le.step) theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H - theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H + protected theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m := le.rec !le.refl (λa b, le.step) @@ -144,18 +144,15 @@ namespace nat theorem zero_lt_succ_iff_true [simp] (n : ℕ) : 0 < succ n ↔ true := iff_true_intro (zero_lt_succ n) - theorem lt.trans {n m k : ℕ} (H1 : n < m) : m < k → n < k := + protected theorem lt.trans {n m k : ℕ} (H1 : n < m) : m < k → n < k := le.trans (le.step H1) - theorem lt_of_le_of_lt {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k := + protected theorem lt_of_le_of_lt {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k := le.trans (succ_le_succ H1) - theorem lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := le.trans + protected theorem lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := le.trans - theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self - - theorem lt_self_iff_false [simp] (n : ℕ) : n < n ↔ false := - iff_false_intro (lt.irrefl n) + protected theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self theorem self_lt_succ (n : ℕ) : n < succ n := !le.refl @@ -165,34 +162,34 @@ namespace nat theorem lt.base (n : ℕ) : n < succ n := !le.refl theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : false := - !lt.irrefl (lt_of_le_of_lt H1 H2) + !lt.irrefl (nat.lt_of_le_of_lt H1 H2) - theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) : m ≤ n → n = m := - le.cases_on H1 (λa, rfl) (λa b c, absurd (lt_of_le_of_lt b c) !lt.irrefl) + protected theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) : m ≤ n → n = m := + le.cases_on H1 (λa, rfl) (λa b c, absurd (nat.lt_of_le_of_lt b c) !lt.irrefl) theorem lt_le_antisymm {n m : ℕ} (H1 : n < m) (H2 : m ≤ n) : false := le_lt_antisymm H2 H1 - theorem lt.asymm {n m : ℕ} (H1 : n < m) : ¬ m < n := - le_lt_antisymm (le_of_lt H1) + protected theorem lt.asymm {n m : ℕ} (H1 : n < m) : ¬ m < n := + le_lt_antisymm (nat.le_of_lt H1) theorem not_lt_zero (a : ℕ) : ¬ a < 0 := !not_succ_le_zero theorem lt_zero_iff_false [simp] (a : ℕ) : a < 0 ↔ false := iff_false_intro (not_lt_zero a) - theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b := + protected theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b := le.cases_on H (inl rfl) (λn h, inr (succ_le_succ h)) - theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b := - or.elim H !le_of_eq !le_of_lt + protected theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b := + or.elim H !nat.le_of_eq !nat.le_of_lt -- less-than is well-founded definition lt.wf [instance] : well_founded lt := well_founded.intro (nat.rec (!acc.intro (λn H, absurd H (not_lt_zero n))) (λn IH, !acc.intro (λm H, - elim (eq_or_lt_of_le (le_of_succ_le_succ H)) + elim (nat.eq_or_lt_of_le (le_of_succ_le_succ H)) (λe, eq.substr e IH) (acc.inv IH)))) definition measure {A : Type} : (A → ℕ) → A → A → Prop := @@ -219,22 +216,23 @@ namespace nat definition decidable_lt [instance] [priority nat.prio] : ∀ a b : nat, decidable (a < b) := λ a b, decidable_le (succ a) b - theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b := + protected theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b := nat.rec (inr !zero_le) (λn, or.rec (λh, inl (le_succ_of_le h)) - (λh, elim (eq_or_lt_of_le h) (λe, inl (eq.subst e !le.refl)) inr)) b + (λh, elim (nat.eq_or_lt_of_le h) (λe, inl (eq.subst e !le.refl)) inr)) b - definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := - by_cases H1 (λh, H2 (elim !lt_or_ge (λa, absurd a h) (λa, a))) + protected definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := + by_cases H1 (λh, H2 (elim !nat.lt_or_ge (λa, absurd a h) (λa, a))) - definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := - lt_ge_by_cases H1 (λh₁, - lt_ge_by_cases H3 (λh₂, H2 (le.antisymm h₂ h₁))) + protected definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) + (H3 : b < a → P) : P := + nat.lt_ge_by_cases H1 (λh₁, + nat.lt_ge_by_cases H3 (λh₂, H2 (le.antisymm h₂ h₁))) - theorem lt.trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a := + protected theorem lt.trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a := lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H)) - theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a := + protected theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a := or.rec_on (lt.trichotomy a b) (λ hlt, absurd hlt hnlt) (λ h, h) diff --git a/library/logic/weak_fan.lean b/library/logic/weak_fan.lean index e6b2b0ba84..408185f0b6 100644 --- a/library/logic/weak_fan.lean +++ b/library/logic/weak_fan.lean @@ -50,7 +50,7 @@ private lemma Y_unique : ∀ {P l₁ l₂}, length l₁ = length l₂ → Y P l | P [] (a₂::l₂) h₁ h₂ h₃ := by contradiction | P (a₁::l₁) [] h₁ h₂ h₃ := by contradiction | P (a₁::l₁) (a₂::l₂) h₁ h₂ h₃ := - have n₁ : length l₁ = length l₂, by rewrite [*length_cons at h₁]; apply add.cancel_right h₁, + have n₁ : length l₁ = length l₂, by rewrite [*length_cons at h₁]; apply add.right_cancel h₁, have n₂ : Y P l₁, from and.elim_left h₂, have n₃ : Y P l₂, from and.elim_left h₃, assert ih : l₁ = l₂, from Y_unique n₁ n₂ n₃,