From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export mathcomp.zify.zify.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]

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.

  (** Next, we show that the maximum of any two natural numbers [m,n] is smaller than
      the sum of the numbers [m + n]. *)
  Lemma max_leq_add m n :
    maxn m n <= m + n.
m, n: nat
maxn m n <= m + n
  Proof.
m, n: nat
maxn m n <= m + n by rewrite geq_max ?leq_addl ?leq_addr. Qed.

  (** For convenience, we observe that the [nat_of_bool] coercion can be dropped
      when establishing equality. *)
  Lemma nat_of_bool_eq (b1 b2 : bool) :
    (nat_of_bool b1 == nat_of_bool b2) = (b1 == b2).
b1, b2: bool
(b1 == b2) = (b1 == b2)
  Proof.
b1, b2: bool
(b1 == b2) = (b1 == b2) by case: b1; case: b2. 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 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 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.