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.