Theorem: LO.FirstOrder.Arith.Model.lt_two_iff_le_one (Arithmetization/Vorspiel/Lemmata.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a < 2 ↔ a ≤ 1
Tactic:
simp [lt_iff_succ_le,
  show a + 1 ≤ 2 ↔ a ≤ 1 from by
    rw[show (2 : M) = 1 + 1 from one_add_one_eq_two.symm]; exact add_le_add_iff_right 1]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a + 1 ≤ 2 ↔ a ≤ 1
Tactic:
rw[show (2 : M) = 1 + 1 from one_add_one_eq_two.symm]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a + 1 ≤ 1 + 1 ↔ a ≤ 1

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a + 1 ≤ 1 + 1 ↔ a ≤ 1
Tactic:
exact add_le_add_iff_right 1
State after:
no goals