Library prosa.util.nat

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

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

  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 →
      m ≤ n - p.

  (* Simplify n + a - b + b - a = n if n ≥ b. *)
  Lemma subn_abba:
    ∀ n a b,
      n ≥ b →
      n + a - b + b - a = n.

  Lemma add_subC:
    ∀ a b c,
      a ≥ c →
      b ≥c →
      a + (b - c ) = a - c + b.

  (* TODO: remove when mathcomp minimum required version becomes 1.10.0 *)
  Lemma ltn_subLR:
    ∀ a b c,
      a - c < b →
      a < b + c.

  (* We can drop additive terms on the lesser side of an inequality. *)
  Lemma leq_addk:
    ∀ m n k,
      n + k ≤ m →
      n ≤ m.

End NatLemmas.

Section Interval.

  (* Trivially, points before the start of an interval, or past the end of an
     interval, are not included in the interval. *)
  Lemma point_not_in_interval:
    ∀ t1 t2 t',
      t2 ≤ t' ∨ t' < t1 →
      ∀ t,
        t1 ≤ t < t2
        → t ≠ t'.

End Interval.

Section NatOrderLemmas.

  (* Mimic the way implicit arguments are used in ssreflect. *)
  Set Implicit Arguments.

  (* ltn_leq_trans: Establish that m < p if m < n and n ≤ p, to mirror the
     lemma leq_ltn_trans in ssrnat.

     NB: There is a good reason for this lemma to be "missing" in ssrnat --
     since m < n is defined as m.+1 ≤ n, ltn_leq_trans is just
     m.+1 ≤ n → n ≤ p → m.+1 ≤ p, that is @leq_trans n m.+1 p.

     Nonetheless we introduce it here because an additional (even though
     arguably redundant) lemma doesn't hurt, and for newcomers the apparent
     absence of the mirror case of leq_ltn_trans can be somewhat confusing.  *)
  Lemma ltn_leq_trans n m p : m < n → n ≤ p → m < p.

End NatOrderLemmas.