Library prosa.classic.util.nat

Require Export prosa.util.nat.

Require Import prosa.classic.util.tactics mathcomp.zify.zify.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.

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

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

  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 ltSnm : ∀ n m, n.+1 < m → n < m.

  Lemma min_lt_same :
    ∀ x y z,
      minn x z < minn y z → x < y.

End NatLemmas.