From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export mathcomp.zify.zify.

Require Export prosa.util.tactics.

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

  (** First, we show that, given [m >= p] and [n >= q], an
      expression [(m + n) - (p + q)] can be transformed into
      expression [(m - p) + (n - q)]. *)
  Lemma subnACA m n p q : p <= m -> q <= n ->
    (m + n) - (p + q) = (m - p) + (n - q).
m, n, p, q: nat
p <= m -> q <= n -> m + n - (p + q) = m - p + (n - q)
  Proof.
m, n, p, q: nat
p <= m -> q <= n -> m + n - (p + q) = m - p + (n - q) by move=> plem qlen; rewrite subnDA addnBAC// addnBA// subnAC. Qed.

  (** Next, we show that [m + p <= n] implies that [m <= n - p]. Note
      that this lemma is similar to ssreflect's lemma [leq_subRL];
      however, the current lemma has no precondition [n <= p], since it
      has only one direction. *)
  Lemma leq_subRL_impl m n p : m + n <= p -> n <= p - m.
m, n, p: nat
m + n <= p -> n <= p - m
  Proof.
m, n, p: nat
m + n <= p -> n <= p - m
    have [mlep|pltm] := leqP m p; first by rewrite leq_subRL.
m, n, p: nat
pltm: p < m
m + n <= p -> n <= p - m
    by move=> /(leq_trans (ltn_addr _ pltm)); rewrite ltnn.
  Qed.

  (** Given constants [a, b, c, z] such that [b <= a], if there is no
      constant [m] such that [a = b + m * c], then it holds that there
      is no constant [n] such that [a + z * c = b + n * c]. *)
  Lemma mul_add_neq a b c z :
    b <= a ->
    (forall m, a <> b + m * c) ->
    forall n, a + z * c <> b + n * c.
a, b, c, z: nat
b <= a ->
(forall m : nat, a <> b + m * c) ->
forall n : nat, a + z * c <> b + n * c
  Proof.
a, b, c, z: nat
b <= a ->
(forall m : nat, a <> b + m * c) ->
forall n : nat, a + z * c <> b + n * c move=> b_le_a + n => /(_ (n - z)); rewrite mulnBl; lia. Qed.

End NatLemmas.

(** In this section, we prove a lemma about intervals of natural
    numbers. *)
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 ->
    forall t,
      t1 <= t < t2 ->
      t <> t'.
t1, t2, t': nat
t2 <= t' \/ t' < t1 ->
forall t : nat, t1 <= t < t2 -> t <> t'
  Proof.
t1, t2, t': nat
t2 <= t' \/ t' < t1 ->
forall t : nat, t1 <= t < t2 -> t <> t'
    move=> excl t /[swap]-> /andP[t1_le_t' t'_lt_t2].
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
False
    have [t2_le_t'|t'_lt_t1] := excl.
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t2_le_t': t2 <= t'
False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1
False
    -
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t2_le_t': t2 <= t'
False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1
False by move: (leq_trans t'_lt_t2 t2_le_t'); rewrite ltnn.
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1
False
    -
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1
False by move: (leq_ltn_trans t1_le_t' t'_lt_t1); rewrite ltnn.
  Qed.

End Interval.

(* [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_deprecated [n m p] : m < n -> n <= p -> m < p.
n, m, p: nat
m < n -> n <= p -> m < p
Proof.
n, m, p: nat
m < n -> n <= p -> m < p exact: leq_trans. Qed.
#[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
Notation ltn_leq_trans := ltn_leq_trans_deprecated.