Library prosa.util.nat
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.util.tactics prosa.util.ssrlia.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 20)
============================
forall m n p : nat, n <= m -> m - n + p = m + p - n
----------------------------------------------------------------------------- *)
Proof. by ins; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma subh2:
∀ m1 m2 n1 n2,
m1 ≥ m2 →
n1 ≥ n2 →
(m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 26)
============================
forall m1 m2 n1 n2 : nat,
m2 <= m1 -> n2 <= n1 -> m1 + n1 - (m2 + n2) = m1 - m2 + (n1 - n2)
----------------------------------------------------------------------------- *)
Proof. by ins; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma subh3:
∀ m n p,
m + p ≤ n →
m ≤ n - p.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 30)
============================
forall m n p : nat, m + p <= n -> m <= n - p
----------------------------------------------------------------------------- *)
Proof.
clear.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 34)
m, n, p : nat
H : m + p <= n
============================
m <= n - p
----------------------------------------------------------------------------- *)
rewrite <- leq_add2r with (p := p).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
m, n, p : nat
H : m + p <= n
============================
m + p <= n - p + p
----------------------------------------------------------------------------- *)
rewrite subh1 //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 41)
m, n, p : nat
H : m + p <= n
============================
m + p <= n + p - p
subgoal 2 (ID 42) is:
p <= n
----------------------------------------------------------------------------- *)
- by rewrite -addnBA // subnn addn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 42)
m, n, p : nat
H : m + p <= n
============================
p <= n
----------------------------------------------------------------------------- *)
- by apply leq_trans with (m+p); first rewrite leq_addl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* Simplify [n + a - b + b - a = n] if [n >= b]. *)
Lemma subn_abba:
∀ n a b,
n ≥ b →
n + a - b + b - a = n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
============================
forall n a b : nat, b <= n -> n + a - b + b - a = n
----------------------------------------------------------------------------- *)
Proof.
move⇒ n a b le_bn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
n, a, b : nat
le_bn : b <= n
============================
n + a - b + b - a = n
----------------------------------------------------------------------------- *)
rewrite subnK;
first by rewrite -addnBA // subnn addn0 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
n, a, b : nat
le_bn : b <= n
============================
b <= n + a
----------------------------------------------------------------------------- *)
rewrite -[b]addn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 88)
n, a, b : nat
le_bn : b <= n
============================
b + 0 <= n + a
----------------------------------------------------------------------------- *)
apply leq_trans with (n := n + 0); rewrite !addn0 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 108)
n, a, b : nat
le_bn : b <= n
============================
n <= n + a
----------------------------------------------------------------------------- *)
apply leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma add_subC:
∀ a b c,
a ≥ c →
b ≥c →
a + (b - c) = a - c + b.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 40)
============================
forall a b c : nat, c <= a -> c <= b -> a + (b - c) = a - c + b
----------------------------------------------------------------------------- *)
Proof.
intros× AgeC BgeC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
a, b, c : nat
AgeC : c <= a
BgeC : c <= b
============================
a + (b - c) = a - c + b
----------------------------------------------------------------------------- *)
induction b;induction c;intros;try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* TODO: remove when mathcomp minimum required version becomes 1.10.0 *)
Lemma ltn_subLR:
∀ a b c,
a - c < b →
a < b + c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
============================
forall a b c : nat, a - c < b -> a < b + c
----------------------------------------------------------------------------- *)
Proof.
intros× AC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
a, b, c : nat
AC : a - c < b
============================
a < b + c
----------------------------------------------------------------------------- *)
ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* We can drop additive terms on the lesser side of an inequality. *)
Lemma leq_addk:
∀ m n k,
n + k ≤ m →
n ≤ m.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
============================
forall m n k : nat, n + k <= m -> n <= m
----------------------------------------------------------------------------- *)
Proof.
move⇒ m n p.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
m, n, p : nat
============================
n + p <= m -> n <= m
----------------------------------------------------------------------------- *)
apply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
m, n, p : nat
============================
n <= n + p
----------------------------------------------------------------------------- *)
by apply leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
For any numbers [a], [b], and [m], either there exists a number [n]
such that [m = a + n * b] or [m <> a + n * b] for any [n].
Lemma exists_or_not_add_mul_cases:
∀ a b m,
(∃ n, m = a + n × b) ∨
(∀ n, m ≠ a + n × b).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
============================
forall a b m : nat,
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
Proof.
move⇒ a b m.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
a, b, m : nat
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
case: (leqP a m) ⇒ LE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 77)
a, b, m : nat
LE : a <= m
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
subgoal 2 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
a, b, m : nat
LE : a <= m
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
case: (boolP(b %| (m - a))) ⇒ DIV.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 89)
a, b, m : nat
LE : a <= m
DIV : b %| m - a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
subgoal 2 (ID 90) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
a, b, m : nat
LE : a <= m
DIV : b %| m - a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
left; ∃ ((m - a) %/ b).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
a, b, m : nat
LE : a <= m
DIV : b %| m - a
============================
m = a + (m - a) %/ b * b
----------------------------------------------------------------------------- *)
now rewrite divnK // subnKC //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 90) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
subgoal 2 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 129)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
============================
forall n : nat, m <> a + n * b
----------------------------------------------------------------------------- *)
move⇒ n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
n : nat
EQ : m = a + n * b
============================
False
----------------------------------------------------------------------------- *)
move: DIV ⇒ /negP DIV; apply DIV.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| m - a
----------------------------------------------------------------------------- *)
rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| a + n * b - a
----------------------------------------------------------------------------- *)
rewrite -addnBAC // subnn add0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 201)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| n * b
----------------------------------------------------------------------------- *)
apply dvdn_mull.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 202)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| b
----------------------------------------------------------------------------- *)
now apply dvdnn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
a, b, m : nat
LE : m < a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
a, b, m : nat
LE : m < a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
right; move⇒ n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 207)
a, b, m : nat
LE : m < a
n : nat
EQ : m = a + n * b
============================
False
----------------------------------------------------------------------------- *)
move: LE; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 211)
a, b, m, n : nat
EQ : m = a + n * b
============================
a + n * b < a -> False
----------------------------------------------------------------------------- *)
now rewrite -ltn_subRL subnn //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ a b m,
(∃ n, m = a + n × b) ∨
(∀ n, m ≠ a + n × b).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
============================
forall a b m : nat,
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
Proof.
move⇒ a b m.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
a, b, m : nat
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
case: (leqP a m) ⇒ LE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 77)
a, b, m : nat
LE : a <= m
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
subgoal 2 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
a, b, m : nat
LE : a <= m
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
case: (boolP(b %| (m - a))) ⇒ DIV.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 89)
a, b, m : nat
LE : a <= m
DIV : b %| m - a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
subgoal 2 (ID 90) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
a, b, m : nat
LE : a <= m
DIV : b %| m - a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
left; ∃ ((m - a) %/ b).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
a, b, m : nat
LE : a <= m
DIV : b %| m - a
============================
m = a + (m - a) %/ b * b
----------------------------------------------------------------------------- *)
now rewrite divnK // subnKC //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 90) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
subgoal 2 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 129)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
============================
forall n : nat, m <> a + n * b
----------------------------------------------------------------------------- *)
move⇒ n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
a, b, m : nat
LE : a <= m
DIV : ~~ (b %| m - a)
n : nat
EQ : m = a + n * b
============================
False
----------------------------------------------------------------------------- *)
move: DIV ⇒ /negP DIV; apply DIV.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| m - a
----------------------------------------------------------------------------- *)
rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| a + n * b - a
----------------------------------------------------------------------------- *)
rewrite -addnBAC // subnn add0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 201)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| n * b
----------------------------------------------------------------------------- *)
apply dvdn_mull.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 202)
a, b, m : nat
LE : a <= m
n : nat
EQ : m = a + n * b
DIV : ~ b %| m - a
============================
b %| b
----------------------------------------------------------------------------- *)
now apply dvdnn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 78) is:
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
a, b, m : nat
LE : m < a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
a, b, m : nat
LE : m < a
============================
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
----------------------------------------------------------------------------- *)
right; move⇒ n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 207)
a, b, m : nat
LE : m < a
n : nat
EQ : m = a + n * b
============================
False
----------------------------------------------------------------------------- *)
move: LE; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 211)
a, b, m, n : nat
EQ : m = a + n * b
============================
a + n * b < a -> False
----------------------------------------------------------------------------- *)
now rewrite -ltn_subRL subnn //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
The expression [n2 * a + b] can be written as [n1 * a + b + (n2 - n1) * a]
for any integer [n1] such that [n1 <= n2].
Lemma add_mul_diff:
∀ n1 n2 a b,
n1 ≤ n2 →
n2 × a + b = n1 × a + b + (n2 - n1) × a.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
============================
forall n1 n2 a b : nat, n1 <= n2 -> n2 * a + b = n1 * a + b + (n2 - n1) * a
----------------------------------------------------------------------------- *)
Proof.
intros × LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n2 * a + b = n1 * a + b + (n2 - n1) * a
----------------------------------------------------------------------------- *)
rewrite mulnBl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n2 * a + b = n1 * a + b + (n2 * a - n1 * a)
----------------------------------------------------------------------------- *)
rewrite addnBA; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 84)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n1 * a <= n2 * a
----------------------------------------------------------------------------- *)
destruct a; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 229)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n1 * a.+1 <= n2 * a.+1
----------------------------------------------------------------------------- *)
now rewrite leq_pmul2r.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ n1 n2 a b,
n1 ≤ n2 →
n2 × a + b = n1 × a + b + (n2 - n1) × a.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
============================
forall n1 n2 a b : nat, n1 <= n2 -> n2 * a + b = n1 * a + b + (n2 - n1) * a
----------------------------------------------------------------------------- *)
Proof.
intros × LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n2 * a + b = n1 * a + b + (n2 - n1) * a
----------------------------------------------------------------------------- *)
rewrite mulnBl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n2 * a + b = n1 * a + b + (n2 * a - n1 * a)
----------------------------------------------------------------------------- *)
rewrite addnBA; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 84)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n1 * a <= n2 * a
----------------------------------------------------------------------------- *)
destruct a; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 229)
n1, n2, a, b : nat
LT : n1 <= n2
============================
n1 * a.+1 <= n2 * a.+1
----------------------------------------------------------------------------- *)
now rewrite leq_pmul2r.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Given constants [a, b, c, z] such that [b <= a] and there is no constant [m]
such that [a = b + m * c], 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 →
(∀ m, a ≠ b + m × c) →
∀ n, a + z × c ≠ b + n × c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
============================
forall a b c z : nat,
b <= a ->
(forall m : nat, a <> b + m * c) -> forall n : nat, a + z * c <> b + n * c
----------------------------------------------------------------------------- *)
Proof.
intros × LTE NEQ n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 82)
a, b, c, z : nat
LTE : b <= a
NEQ : forall m : nat, a <> b + m * c
n : nat
EQ : a + z * c = b + n * c
============================
False
----------------------------------------------------------------------------- *)
specialize (NEQ (n - z)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 84)
a, b, c, z : nat
LTE : b <= a
n : nat
NEQ : a <> b + (n - z) * c
EQ : a + z * c = b + n * c
============================
False
----------------------------------------------------------------------------- *)
rewrite mulnBl in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
a, b, c, z : nat
LTE : b <= a
n : nat
EQ : a + z * c = b + n * c
NEQ : a <> b + (n * c - z * c)
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 21)
============================
forall t1 t2 t' : nat,
t2 <= t' \/ t' < t1 -> forall t : nat, t1 <= t < t2 -> t <> t'
----------------------------------------------------------------------------- *)
Proof.
move⇒ t1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
t1, t2, t' : nat
EXCLUDED : t2 <= t' \/ t' < t1
t : nat
GEQ_t1 : t1 <= t
LT_t2 : t < t2
EQ : t = t'
============================
False
----------------------------------------------------------------------------- *)
subst.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
t1, t2, t' : nat
EXCLUDED : t2 <= t' \/ t' < t1
LT_t2 : t' < t2
GEQ_t1 : t1 <= t'
============================
False
----------------------------------------------------------------------------- *)
case EXCLUDED ⇒ [INEQ | INEQ];
eapply leq_ltn_trans in INEQ; eauto;
by rewrite ltnn in INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Interval.
Section NatOrderLemmas.
(* Mimic the way implicit arguments are used in [ssreflect]. *)
Set Implicit Arguments.
Unset Strict Implicit.
(* [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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 22)
n, m, p : nat
============================
m < n -> n <= p -> m < p
----------------------------------------------------------------------------- *)
Proof. exact (@leq_trans n m.+1 p).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End NatOrderLemmas.
∀ a b c z,
b ≤ a →
(∀ m, a ≠ b + m × c) →
∀ n, a + z × c ≠ b + n × c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
============================
forall a b c z : nat,
b <= a ->
(forall m : nat, a <> b + m * c) -> forall n : nat, a + z * c <> b + n * c
----------------------------------------------------------------------------- *)
Proof.
intros × LTE NEQ n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 82)
a, b, c, z : nat
LTE : b <= a
NEQ : forall m : nat, a <> b + m * c
n : nat
EQ : a + z * c = b + n * c
============================
False
----------------------------------------------------------------------------- *)
specialize (NEQ (n - z)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 84)
a, b, c, z : nat
LTE : b <= a
n : nat
NEQ : a <> b + (n - z) * c
EQ : a + z * c = b + n * c
============================
False
----------------------------------------------------------------------------- *)
rewrite mulnBl in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
a, b, c, z : nat
LTE : b <= a
n : nat
EQ : a + z * c = b + n * c
NEQ : a <> b + (n * c - z * c)
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 21)
============================
forall t1 t2 t' : nat,
t2 <= t' \/ t' < t1 -> forall t : nat, t1 <= t < t2 -> t <> t'
----------------------------------------------------------------------------- *)
Proof.
move⇒ t1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
t1, t2, t' : nat
EXCLUDED : t2 <= t' \/ t' < t1
t : nat
GEQ_t1 : t1 <= t
LT_t2 : t < t2
EQ : t = t'
============================
False
----------------------------------------------------------------------------- *)
subst.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
t1, t2, t' : nat
EXCLUDED : t2 <= t' \/ t' < t1
LT_t2 : t' < t2
GEQ_t1 : t1 <= t'
============================
False
----------------------------------------------------------------------------- *)
case EXCLUDED ⇒ [INEQ | INEQ];
eapply leq_ltn_trans in INEQ; eauto;
by rewrite ltnn in INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Interval.
Section NatOrderLemmas.
(* Mimic the way implicit arguments are used in [ssreflect]. *)
Set Implicit Arguments.
Unset Strict Implicit.
(* [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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 22)
n, m, p : nat
============================
m < n -> n <= p -> m < p
----------------------------------------------------------------------------- *)
Proof. exact (@leq_trans n m.+1 p).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End NatOrderLemmas.