Theory Nat_Util

theory Nat_Util
  imports Main
begin

section ‹HOL›

lemma duplicate_assms:
  "(⟦P; P⟧ ⟹ Q) ≡ (P ⟹ Q)"
  by simp

section ‹Natural Number Arithmetic›

lemma div_2_eq_Suc:
  "⟦x div 2 = y div 2; x ≠ y⟧ ⟹ (y = Suc x) ∨ (x = Suc y)"
  by linarith

lemma Suc_m_sub_n_div_2:
  "Suc ((m - n) div 2) > (m - Suc n) div 2"
  by (simp add: div_le_mono le_Suc_eq)

lemma Suc_div_2_less_Suc:
  "Suc x div 2 < Suc x"
  by simp

lemma nat_x_less_y_le_Suc_x:
  "⟦x < y; y ≤ Suc x⟧ ⟹ y = Suc x"
  by simp

lemma nat_sub_eq_add:
  "⟦(a :: nat) - b = c - d; b < a⟧ ⟹ a + d = c + b"
  by simp

end