Skip to content

Commit

Permalink
chore(set_theory/game/*): Protect ambiguous lemmas (#13557)
Browse files Browse the repository at this point in the history 
Protect `pgame.neg_zero` and inline `pgame.add_le_add_left` and friends into `covariant_class` instances.



Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
  • Loading branch information
@YaelDillies @vihdzp
YaelDillies and vihdzp committed Apr 21, 2022
1 parent b6c96ef commit b7cba57
Show file tree
Hide file tree
Showing 5 changed files with 92 additions and 81 deletions.
24 changes: 13 additions & 11 deletions src/set_theory/game/basic.lean
View file
Expand Up @@ -22,6 +22,8 @@ not imply `(x*z).equiv (y*z)`. Hence, multiplication is not a well-defined opera
Nevertheless, the abelian group structure on games allows us to simplify many proofs for pre-games.
-/

open function

universes u

local infix ` ≈ ` := pgame.equiv
Expand Down Expand Up @@ -145,8 +147,11 @@ instance : add_comm_group game :=
{ ..game.add_comm_semigroup,
..game.add_group }

theorem add_le_add_left : ∀ (a b : game), a ≤ b → ∀ (c : game), c + a ≤ c + b :=
begin rintro ⟨a⟩ ⟨b⟩ h ⟨c⟩, apply pgame.add_le_add_left h, end
instance covariant_class_add_le : covariant_class game game (+) (≤) :=
⟨begin rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ h, exact @add_le_add_left _ _ _ _ b c h a end⟩

instance covariant_class_swap_add_le : covariant_class game game (swap (+)) (≤) :=
⟨begin rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ h, exact @add_le_add_right _ _ _ _ b c h a end⟩

-- While it is very tempting to define a `partial_order` on games, and prove
-- that games form an `ordered_add_comm_group`, it is a bit dangerous.
Expand All @@ -169,7 +174,7 @@ def game_partial_order : partial_order game :=

/-- The `<` operation provided by this `ordered_add_comm_group` is not the usual `<` on games! -/
def ordered_add_comm_group_game : ordered_add_comm_group game :=
{ add_le_add_left := add_le_add_left,
{ add_le_add_left := @add_le_add_left _ _ _ game.covariant_class_add_le,
..game.add_comm_group,
..game_partial_order }

Expand Down Expand Up @@ -277,18 +282,15 @@ begin
... ≃ yl × xr ⊕ yr × xl : equiv.sum_congr (equiv.prod_comm _ _) (equiv.prod_comm _ _),
{ rintro (⟨i, j⟩ | ⟨i, j⟩),
{ change ⟦xL i * y⟧ + ⟦x * yL j⟧ - ⟦xL i * yL j⟧ = ⟦yL j * x⟧ + ⟦y * xL i⟧ - ⟦yL j * xL i⟧,
rw [quot_mul_comm (xL i) y, quot_mul_comm x (yL j), quot_mul_comm (xL i) (yL j)],
abel },
rw [quot_mul_comm (xL i) y, quot_mul_comm x (yL j), quot_mul_comm (xL i) (yL j), add_comm] },
{ change ⟦xR i * y⟧ + ⟦x * yR j⟧ - ⟦xR i * yR j⟧ = ⟦yR j * x⟧ + ⟦y * xR i⟧ - ⟦yR j * xR i⟧,
rw [quot_mul_comm (xR i) y, quot_mul_comm x (yR j), quot_mul_comm (xR i) (yR j)],
abel } },
rw [quot_mul_comm (xR i) y, quot_mul_comm x (yR j), quot_mul_comm (xR i) (yR j),
add_comm] } },
{ rintro (⟨j, i⟩ | ⟨j, i⟩),
{ change ⟦xR i * y⟧ + ⟦x * yL j⟧ - ⟦xR i * yL j⟧ = ⟦yL j * x⟧ + ⟦y * xR i⟧ - ⟦yL j * xR i⟧,
rw [quot_mul_comm (xR i) y, quot_mul_comm x (yL j), quot_mul_comm (xR i) (yL j)],
abel },
rw [quot_mul_comm (xR i) y, quot_mul_comm x (yL j), quot_mul_comm (xR i) (yL j), add_comm] },
{ change ⟦xL i * y⟧ + ⟦x * yR j⟧ - ⟦xL i * yR j⟧ = ⟦yR j * x⟧ + ⟦y * xL i⟧ - ⟦yR j * xL i⟧,
rw [quot_mul_comm (xL i) y, quot_mul_comm x (yR j), quot_mul_comm (xL i) (yR j)],
abel } }
rw [quot_mul_comm (xL i) y, quot_mul_comm x (yR j), quot_mul_comm (xL i) (yR j), add_comm] } }
end
using_well_founded { dec_tac := pgame_wf_tac }

Expand Down
6 changes: 3 additions & 3 deletions src/set_theory/game/impartial.lean
View file
Expand Up @@ -107,12 +107,12 @@ begin
{ cases hl with hpos hnonneg,
rw ←not_lt at hnonneg,
have hneg := lt_of_lt_of_equiv hpos (neg_equiv_self G),
rw [lt_iff_neg_gt, neg_neg, neg_zero] at hneg,
rw [lt_iff_neg_gt, neg_neg, pgame.neg_zero] at hneg,
contradiction },
{ cases hr with hnonpos hneg,
rw ←not_lt at hnonpos,
have hpos := lt_of_equiv_of_lt (neg_equiv_self G).symm hneg,
rw [lt_iff_neg_gt, neg_neg, neg_zero] at hpos,
rw [lt_iff_neg_gt, neg_neg, pgame.neg_zero] at hpos,
contradiction },
{ left, assumption },
{ right, assumption }
Expand Down Expand Up @@ -152,7 +152,7 @@ lemma le_zero_iff {G : pgame} [G.impartial] : G ≤ 0 ↔ 0 ≤ G :=
by rw [le_zero_iff_zero_le_neg, le_congr (equiv_refl 0) (neg_equiv_self G)]

lemma lt_zero_iff {G : pgame} [G.impartial] : G < 0 ↔ 0 < G :=
by rw [lt_iff_neg_gt, neg_zero, lt_congr (equiv_refl 0) (neg_equiv_self G)]
by rw [lt_iff_neg_gt, pgame.neg_zero, lt_congr (equiv_refl 0) (neg_equiv_self G)]

lemma first_loses_symm (G : pgame) [G.impartial] : G.first_loses ↔ G ≤ 0 :=
⟨and.left, λ h, ⟨h, le_zero_iff.1 h⟩⟩
Expand Down
97 changes: 53 additions & 44 deletions src/set_theory/game/pgame.lean
View file
Expand Up @@ -104,6 +104,8 @@ An interested reader may like to formalise some of the material from
* [André Joyal, *Remarques sur la théorie des jeux à deux personnes*][joyal1997]
-/

open function

universes u

/-- The type of pre-games, before we have quotiented
Expand Down Expand Up @@ -479,6 +481,8 @@ inductive restricted : pgame.{u} → pgame.{u} → Type (u+1)
(λ i, restricted.refl _) (λ j, restricted.refl _)
using_well_founded { dec_tac := pgame_wf_tac }

instance (x : pgame) : inhabited (restricted x x) := ⟨restricted.refl _⟩

-- TODO trans for restricted

theorem restricted.le : Π {x y : pgame} (r : restricted x y), x ≤ y
Expand All @@ -504,7 +508,7 @@ inductive relabelling : pgame.{u} → pgame.{u} → Type (u+1)

/-- If `x` is a relabelling of `y`, then Left and Right have the same moves in either game,
so `x` is a restriction of `y`. -/
def relabelling.restricted: Π {x y : pgame} (r : relabelling x y), restricted x y
def relabelling.restricted : Π {x y : pgame} (r : relabelling x y), restricted x y
| (mk xl xr xL xR) (mk yl yr yL yR) (relabelling.mk L_equiv R_equiv L_relabelling R_relabelling) :=
restricted.mk L_equiv.to_embedding R_equiv.symm.to_embedding
(λ i, (L_relabelling i).restricted)
Expand All @@ -521,6 +525,8 @@ restricted.mk L_equiv.to_embedding R_equiv.symm.to_embedding
(λ i, relabelling.refl _) (λ j, relabelling.refl _)
using_well_founded { dec_tac := pgame_wf_tac }

instance (x : pgame) : inhabited (relabelling x x) := ⟨relabelling.refl _⟩

/-- Reverse a relabelling. -/
@[symm] def relabelling.symm : Π {x y : pgame}, relabelling x y → relabelling y x
| (mk xl xr xL xR) (mk yl yr yL yR) (relabelling.mk L_equiv R_equiv L_relabelling R_relabelling) :=
Expand Down Expand Up @@ -587,14 +593,15 @@ instance : has_neg pgame := ⟨neg⟩
@[simp] lemma neg_def {xl xr xL xR} : -(mk xl xr xL xR) = mk xr xl (λ j, -(xR j)) (λ i, -(xL i)) :=
rfl

@[simp] theorem neg_neg : Π {x : pgame}, -(-x) = x
| (mk xl xr xL xR) :=
begin
dsimp [has_neg.neg, neg],
congr; funext i; apply neg_neg
end
instance : has_involutive_neg pgame :=
{ neg_neg := λ x, begin
induction x with xl xr xL xR ihL ihR,
simp_rw [neg_def, ihL, ihR],
exact ⟨rfl, rfl, heq.rfl, heq.rfl⟩,
end,
..pgame.has_neg }

@[simp] theorem neg_zero : -(0 : pgame) = 0 :=
@[simp] protected lemma neg_zero : -(0 : pgame) = 0 :=
begin
dsimp [has_zero.zero, has_neg.neg, neg],
congr; funext i; cases i
Expand All @@ -613,7 +620,7 @@ by { cases x, refl }
move_right x ((left_moves_neg x) i) = -(move_left (-x) i) :=
begin
induction x,
exact neg_neg.symm
exact (neg_neg _).symm
end
@[simp] lemma move_left_left_moves_neg_symm {x : pgame} (i : right_moves x) :
move_left (-x) ((left_moves_neg x).symm i) = -(move_right x i) :=
Expand All @@ -622,7 +629,7 @@ by { cases x, refl }
move_left x ((right_moves_neg x) i) = -(move_right (-x) i) :=
begin
induction x,
exact neg_neg.symm
exact (neg_neg _).symm
end
@[simp] lemma move_right_right_moves_neg_symm {x : pgame} (i : left_moves x) :
move_right (-x) ((right_moves_neg x).symm i) = -(move_left x i) :=
Expand Down Expand Up @@ -683,13 +690,13 @@ end
theorem zero_le_iff_neg_le_zero {x : pgame} : 0 ≤ x ↔ -x ≤ 0 :=
begin
convert le_iff_neg_ge,
rw neg_zero
rw pgame.neg_zero
end

theorem le_zero_iff_zero_le_neg {x : pgame} : x ≤ 0 ↔ 0 ≤ -x :=
begin
convert le_iff_neg_ge,
rw neg_zero
rw pgame.neg_zero
end

/-- The sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
Expand Down Expand Up @@ -871,7 +878,7 @@ using_well_founded { dec_tac := pgame_wf_tac }
theorem add_assoc_equiv {x y z : pgame} : (x + y) + z ≈ x + (y + z) :=
(add_assoc_relabelling x y z).equiv

theorem add_le_add_right : Π {x y z : pgame} (h : x ≤ y), x + z ≤ y + z
private lemma add_le_add_right : Π {x y z : pgame} (h : x ≤ y), x + z ≤ y + z
| (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
begin
intros h,
Expand Down Expand Up @@ -920,16 +927,19 @@ begin
end
using_well_founded { dec_tac := pgame_wf_tac }

theorem add_le_add_left {x y z : pgame} (h : y ≤ z) : x + y ≤ x + z :=
calc x + y ≤ y + x : add_comm_le
... ≤ z + x : add_le_add_right h
... ≤ x + z : add_comm_le
instance covariant_class_swap_add_le : covariant_class pgame pgame (swap (+)) (≤) :=
⟨λ x y z, add_le_add_right⟩

instance covariant_class_add_le : covariant_class pgame pgame (+) (≤) :=
⟨λ x y z h, calc x + y ≤ y + x : add_comm_le
... ≤ z + x : add_le_add_right h _
... ≤ x + z : add_comm_le⟩

theorem add_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w + y ≈ x + z :=
⟨calc w + y ≤ w + z : add_le_add_left h₂.1
... ≤ x + z : add_le_add_right h₁.1,
calc x + z ≤ x + y : add_le_add_left h₂.2
... ≤ w + y : add_le_add_right h₁.2⟩
⟨calc w + y ≤ w + z : add_le_add_left h₂.1 _
... ≤ x + z : add_le_add_right h₁.1 _,
calc x + z ≤ x + y : add_le_add_left h₂.2 _
... ≤ w + y : add_le_add_right h₁.2 _⟩

theorem sub_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w - y ≈ x - z :=
add_congr h₁ (neg_congr h₂)
Expand Down Expand Up @@ -960,7 +970,7 @@ using_well_founded { dec_tac := pgame_wf_tac }
theorem zero_le_add_left_neg : Π {x : pgame}, 0 ≤ (-x) + x :=
begin
intro x,
rw [le_iff_neg_ge, neg_zero],
rw [le_iff_neg_ge, pgame.neg_zero],
exact le_trans neg_add_le add_left_neg_le_zero
end

Expand All @@ -978,37 +988,36 @@ calc 0 ≤ (-x) + x : zero_le_add_left_neg
theorem add_right_neg_equiv {x : pgame} : x + (-x) ≈ 0 :=
⟨add_right_neg_le_zero, zero_le_add_right_neg⟩

theorem add_lt_add_right {x y z : pgame} (h : x < y) : x + z < y + z :=
suffices y + z ≤ x + z → y ≤ x, by { rw ←not_le at ⊢ h, exact mt this h },
assume w,
calc y ≤ y + 0 : (add_zero_relabelling _).symm.le
... ≤ y + (z + -z) : add_le_add_left zero_le_add_right_neg
... ≤ (y + z) + (-z) : (add_assoc_relabelling _ _ _).symm.le
... ≤ (x + z) + (-z) : add_le_add_right w
... ≤ x + (z + -z) : (add_assoc_relabelling _ _ _).le
... ≤ x + 0 : add_le_add_left add_right_neg_le_zero
... ≤ x : (add_zero_relabelling _).le

theorem add_lt_add_left {x y z : pgame} (h : y < z) : x + y < x + z :=
calc x + y ≤ y + x : add_comm_le
... < z + x : add_lt_add_right h
... ≤ x + z : add_comm_le
instance covariant_class_swap_add_lt : covariant_class pgame pgame (swap (+)) (<) :=
⟨λ x y z h, suffices z + x ≤ y + x → z ≤ y, by { rw ←not_le at ⊢ h, exact mt this h }, λ w,
calc z ≤ z + 0 : (add_zero_relabelling _).symm.le
... ≤ z + (x + -x) : add_le_add_left zero_le_add_right_neg _
... ≤ z + x + -x : (add_assoc_relabelling _ _ _).symm.le
... ≤ y + x + -x : add_le_add_right w _
... ≤ y + (x + -x) : (add_assoc_relabelling _ _ _).le
... ≤ y + 0 : add_le_add_left add_right_neg_le_zero _
... ≤ y : (add_zero_relabelling _).le⟩

instance covariant_class_add_lt : covariant_class pgame pgame (+) (<) :=
⟨λ x y z h, calc x + y ≤ y + x : add_comm_le
... < z + x : add_lt_add_right h _
... ≤ x + z : add_comm_le⟩

theorem le_iff_sub_nonneg {x y : pgame} : x ≤ y ↔ 0 ≤ y - x :=
⟨λ h, le_trans zero_le_add_right_neg (add_le_add_right h),
⟨λ h, le_trans zero_le_add_right_neg (add_le_add_right h _),
λ h,
calc x ≤ 0 + x : (zero_add_relabelling x).symm.le
... ≤ (y - x) + x : add_le_add_right h
... ≤ y - x + x : add_le_add_right h _
... ≤ y + (-x + x) : (add_assoc_relabelling _ _ _).le
... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero)
... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero) _
... ≤ y : (add_zero_relabelling y).le⟩
theorem lt_iff_sub_pos {x y : pgame} : x < y ↔ 0 < y - x :=
⟨λ h, lt_of_le_of_lt zero_le_add_right_neg (add_lt_add_right h),
⟨λ h, lt_of_le_of_lt zero_le_add_right_neg (add_lt_add_right h _),
λ h,
calc x ≤ 0 + x : (zero_add_relabelling x).symm.le
... < (y - x) + x : add_lt_add_right h
... < y - x + x : add_lt_add_right h _
... ≤ y + (-x + x) : (add_assoc_relabelling _ _ _).le
... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero)
... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero) _
... ≤ y : (add_zero_relabelling y).le⟩

/-- The pre-game `star`, which is fuzzy/confused with zero. -/
Expand Down Expand Up @@ -1039,7 +1048,7 @@ def half : pgame := ⟨punit, punit, 0, 1⟩

@[simp] lemma half_move_right : half.move_right punit.star = 1 := rfl

theorem zero_lt_half : 0 < half :=
protected theorem zero_lt_half : 0 < half :=
begin
rw lt_def,
left,
Expand Down
32 changes: 16 additions & 16 deletions src/set_theory/surreal/basic.lean
View file
Expand Up @@ -144,41 +144,41 @@ begin
{ left,
use (left_moves_add x z).symm (sum.inl ix),
simp only [add_move_left_inl],
calc w + y ≤ move_left x ix + y : add_le_add_right hix
... ≤ move_left x ix + move_left z iz : add_le_add_left hiz
... ≤ move_left x ix + z : add_le_add_left (oz.move_left_le iz) },
calc w + y ≤ move_left x ix + y : add_le_add_right hix _
... ≤ move_left x ix + move_left z iz : add_le_add_left hiz _
... ≤ move_left x ix + z : add_le_add_left (oz.move_left_le iz) _ },
{ left,
use (left_moves_add x z).symm (sum.inl ix),
simp only [add_move_left_inl],
calc w + y ≤ move_left x ix + y : add_le_add_right hix
... ≤ move_left x ix + move_right y jy : add_le_add_left (oy.le_move_right jy)
... ≤ move_left x ix + z : add_le_add_left hjy },
calc w + y ≤ move_left x ix + y : add_le_add_right hix _
... ≤ move_left x ix + move_right y jy : add_le_add_left (oy.le_move_right jy) _
... ≤ move_left x ix + z : add_le_add_left hjy _ },
{ right,
use (right_moves_add w y).symm (sum.inl jw),
simp only [add_move_right_inl],
calc move_right w jw + y ≤ x + y : add_le_add_right hjw
... ≤ x + move_left z iz : add_le_add_left hiz
... ≤ x + z : add_le_add_left (oz.move_left_le iz), },
calc move_right w jw + y ≤ x + y : add_le_add_right hjw _
... ≤ x + move_left z iz : add_le_add_left hiz _
... ≤ x + z : add_le_add_left (oz.move_left_le iz) _ },
{ right,
use (right_moves_add w y).symm (sum.inl jw),
simp only [add_move_right_inl],
calc move_right w jw + y ≤ x + y : add_le_add_right hjw
... ≤ x + move_right y jy : add_le_add_left (oy.le_move_right jy)
... ≤ x + z : add_le_add_left hjy, },
calc move_right w jw + y ≤ x + y : add_le_add_right hjw _
... ≤ x + move_right y jy : add_le_add_left (oy.le_move_right jy) _
... ≤ x + z : add_le_add_left hjy _ },
end

theorem numeric_add : Π {x y : pgame} (ox : numeric x) (oy : numeric y), numeric (x + y)
| ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ ox oy :=
⟨begin
rintros (ix|iy) (jx|jy),
{ show xL ix + ⟨yl, yr, yL, yR⟩ < xR jx + ⟨yl, yr, yL, yR⟩,
exact add_lt_add_right (ox.1 ix jx), },
exact add_lt_add_right (ox.1 ix jx) _ },
{ show xL ix + ⟨yl, yr, yL, yR⟩ < ⟨xl, xr, xL, xR⟩ + yR jy,
exact add_lt_add oy (oy.move_right jy) (ox.move_left_lt _) (oy.lt_move_right _), },
{ -- show ⟨xl, xr, xL, xR⟩ + yL iy < xR jx + ⟨yl, yr, yL, yR⟩, -- fails?
exact add_lt_add (oy.move_left iy) oy (ox.lt_move_right _) (oy.move_left_lt _), },
{ -- show ⟨xl, xr, xL, xR⟩ + yL iy < ⟨xl, xr, xL, xR⟩ + yR jy, -- fails?
exact @add_lt_add_left ⟨xl, xr, xL, xR⟩ _ _ (oy.1 iy jy), }
exact @add_lt_add_left pgame _ _ _ _ _ (oy.1 iy jy) ⟨xl, xr, xL, xR⟩ }
end,
begin
split,
Expand Down Expand Up @@ -233,7 +233,7 @@ begin
{ rintro ⟨ ⟩,
left,
use (sum.inl punit.star),
calc 0 ≤ half : le_of_lt numeric_zero numeric_half zero_lt_half
calc 0 ≤ half : le_of_lt numeric_zero numeric_half pgame.zero_lt_half
... ≈ 0 + half : (zero_add_equiv half).symm
... = (half + half).move_left (sum.inl punit.star) : by fsplit },
{ rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩); left,
Expand Down Expand Up @@ -327,7 +327,7 @@ instance : ordered_add_comm_group surreal :=
le_trans := by { rintros ⟨_⟩ ⟨_⟩ ⟨_⟩, exact pgame.le_trans },
lt_iff_le_not_le := by { rintros ⟨_, ox⟩ ⟨_, oy⟩, exact pgame.lt_iff_le_not_le ox oy },
le_antisymm := by { rintros ⟨_⟩ ⟨_⟩ h₁ h₂, exact quotient.sound ⟨h₁, h₂⟩ },
add_le_add_left := by { rintros ⟨_⟩ ⟨_⟩ hx ⟨_⟩, exact pgame.add_le_add_left hx } }
add_le_add_left := by { rintros ⟨_⟩ ⟨_⟩ hx ⟨_⟩, exact @add_le_add_left pgame _ _ _ _ _ hx _ } }

noncomputable instance : linear_ordered_add_comm_group surreal :=
{ le_total := by rintro ⟨⟨x, ox⟩⟩ ⟨⟨y, oy⟩⟩; classical; exact
Expand Down
14 changes: 7 additions & 7 deletions src/set_theory/surreal/dyadic.lean
View file
Expand Up @@ -97,19 +97,19 @@ begin
right,
use sum.inl punit.star,
calc pow_half (n.succ) + pow_half (n.succ + 1)
≤ pow_half (n.succ) + pow_half (n.succ) : add_le_add_left pow_half_succ_le_pow_half
≤ pow_half (n.succ) + pow_half (n.succ) : add_le_add_left pow_half_succ_le_pow_half _
... ≈ pow_half n : hn },
{ rintro ⟨ ⟩,
calc 0 ≈ 0 + 0 : (add_zero_equiv _).symm
... ≤ pow_half (n.succ + 1) + 0 : add_le_add_right zero_le_pow_half
... < pow_half (n.succ + 1) + pow_half (n.succ + 1) : add_lt_add_left zero_lt_pow_half },
... ≤ pow_half (n.succ + 1) + 0 : add_le_add_right zero_le_pow_half _
... < pow_half (n.succ + 1) + pow_half (n.succ + 1) : add_lt_add_left zero_lt_pow_half _ },
{ rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩),
{ calc pow_half n.succ
≈ pow_half n.succ + 0 : (add_zero_equiv _).symm
... < pow_half (n.succ) + pow_half (n.succ + 1) : add_lt_add_left zero_lt_pow_half },
≈ pow_half n.succ + 0 : (add_zero_equiv _).symm
... < pow_half (n.succ) + pow_half (n.succ + 1) : add_lt_add_left zero_lt_pow_half _ },
{ calc pow_half n.succ
≈ 0 + pow_half n.succ : (zero_add_equiv _).symm
... < pow_half (n.succ + 1) + pow_half (n.succ) : add_lt_add_right zero_lt_pow_half }}}
≈ 0 + pow_half n.succ : (zero_add_equiv _).symm
... < pow_half (n.succ + 1) + pow_half (n.succ) : add_lt_add_right zero_lt_pow_half _ } } }
end

end pgame
Expand Down

0 comments on commit b7cba57

Please sign in to comment.