Library rt.util.nat

Require Import rt.util.tactics rt.util.divround rt.util.ssromega.

(* Additional lemmas about natural numbers. *)
Section NatLemmas.

  Lemma addnb (b1 b2 : bool) : (b1 + b2) != 0 = b1 || b2.

  Lemma subh1 :
    ∀ m n p,
      m ≥ n →
      m - n + p = m + p - n.

  Lemma subh2 :
    ∀ m1 m2 n1 n2,
      m1 ≥ m2 →
      n1 ≥ n2 →
      (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).

  Lemma subh3 :
    ∀ m n p,
      m + p ≤ n →
      n ≥ p →
      m ≤ n - p.

  Lemma subh4:
    ∀ m n p,
      m ≤ n →
      p ≤ n →
      (m == n - p) = (p == n - m).

  Lemma addmovr:
    ∀ m n p,
      m ≥ n →
      (m - n = p ↔ m = p + n).

  Lemma addmovl:
    ∀ m n p,
      m ≥ n →
      (p = m - n ↔ p + n = m).

  Lemma ltn_div_trunc :
    ∀ m n d,
      d > 0 →
      m %/ d < n %/ d →
      m < n.

  Lemma subndiv_eq_mod:
    ∀ n d, n - n %/ d × d = n %% d.

  Lemma ltSnm : ∀ n m, n.+1 < m → n < m.

  Lemma divSn_cases :
    ∀ n d,
      d > 1 →
      (n %/ d = n.+1 %/d ∧ n %% d + 1 = n.+1 %% d) ∨
      (n %/ d + 1 = n.+1 %/ d).
 Case 1: y = d - 1*)
 Case 2: y < d - 1 *)
  Lemma ceil_neq0 :
    ∀ x y,
      x > 0 →
      y > 0 →
      div_ceil x y > 0.

  Lemma leq_divceil2r :
    ∀ d m n,
      d > 0 →
      m ≤ n →
      div_ceil m d ≤ div_ceil n d.
  Lemma min_lt_same :
    ∀ x y z,
      minn x z < minn y z → x < y.

End NatLemmas.