NSub.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Export NMulOrder.

Module Type NSubProp (Import N : NAxiomsMiniSig').
Include NMulOrderProp N.

Theorem sub_0_l : forall n, 0 - n == 0.forall n : t, 0 - n == 0
Proof.forall n : t, 0 - n == 0
induct n.0 - 0 == 0
forall n : t, 0 - n == 0 -> 0 - S n == 0
apply sub_0_r.forall n : t, 0 - n == 0 -> 0 - S n == 0
intros n IH; rewrite sub_succ_r; rewrite IH.n:t
IH:0 - n == 0
P 0 == 0 now apply pred_0.
Qed.

Theorem sub_succ : forall n m, S n - S m == n - m.forall n m : t, S n - S m == n - m
Proof.forall n m : t, S n - S m == n - m
intro n; induct m.n:t
S n - S 0 == n - 0
n:t
forall n0 : t,
S n - S n0 == n - n0 -> S n - S (S n0) == n - S n0
rewrite sub_succ_r.n:t
P (S n - 0) == n - 0
n:t
forall n0 : t,
S n - S n0 == n - n0 -> S n - S (S n0) == n - S n0 do 2 rewrite sub_0_r.n:t
P (S n) == n
n:t
forall n0 : t,
S n - S n0 == n - n0 -> S n - S (S n0) == n - S n0 now rewrite pred_succ.n:t
forall n0 : t,
S n - S n0 == n - n0 -> S n - S (S n0) == n - S n0
intros m IH.n, m:t
IH:S n - S m == n - m
S n - S (S m) == n - S m rewrite sub_succ_r.n, m:t
IH:S n - S m == n - m
P (S n - S m) == n - S m rewrite IH.n, m:t
IH:S n - S m == n - m
P (n - m) == n - S m now rewrite sub_succ_r.
Qed.

Theorem sub_diag : forall n, n - n == 0.forall n : t, n - n == 0
Proof.forall n : t, n - n == 0
induct n.0 - 0 == 0
forall n : t, n - n == 0 -> S n - S n == 0 apply sub_0_r.forall n : t, n - n == 0 -> S n - S n == 0 intros n IH; rewrite sub_succ; now rewrite IH.
Qed.

Theorem sub_gt : forall n m, n > m -> n - m ~= 0.forall n m : t, m < n -> n - m ~= 0
Proof.forall n m : t, m < n -> n - m ~= 0
intros n m H; elim H using lt_ind_rel; clear n m H.Proper (eq ==> eq ==> iff) (fun m n : t => n - m ~= 0)
forall m : t, S m - 0 ~= 0
forall n m : t, n < m -> m - n ~= 0 -> S m - S n ~= 0
solve_proper.forall m : t, S m - 0 ~= 0
forall n m : t, n < m -> m - n ~= 0 -> S m - S n ~= 0
intro; rewrite sub_0_r; apply neq_succ_0.forall n m : t, n < m -> m - n ~= 0 -> S m - S n ~= 0
intros; now rewrite sub_succ.
Qed.

Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p.forall n m p : t, p <= m -> n + (m - p) == n + m - p
Proof.forall n m p : t, p <= m -> n + (m - p) == n + m - p
intros n m p; induct p.n, m:t
0 <= m -> n + (m - 0) == n + m - 0
n, m:t
forall n0 : t,
(n0 <= m -> n + (m - n0) == n + m - n0) ->
S n0 <= m -> n + (m - S n0) == n + m - S n0
intro; now do 2 rewrite sub_0_r.n, m:t
forall n0 : t,
(n0 <= m -> n + (m - n0) == n + m - n0) ->
S n0 <= m -> n + (m - S n0) == n + m - S n0
intros p IH H.n, m, p:t
IH:p <= m -> n + (m - p) == n + m - p
H:S p <= m
n + (m - S p) == n + m - S p do 2 rewrite sub_succ_r.n, m, p:t
IH:p <= m -> n + (m - p) == n + m - p
H:S p <= m
n + P (m - p) == P (n + m - p)
rewrite <- IH by (apply lt_le_incl; now apply le_succ_l).n, m, p:t
IH:p <= m -> n + (m - p) == n + m - p
H:S p <= m
n + P (m - p) == P (n + (m - p))
rewrite add_pred_r by (apply sub_gt; now apply le_succ_l).n, m, p:t
IH:p <= m -> n + (m - p) == n + m - p
H:S p <= m
P (n + (m - p)) == P (n + (m - p))
reflexivity.
Qed.

Theorem sub_succ_l : forall n m, n <= m -> S m - n == S (m - n).forall n m : t, n <= m -> S m - n == S (m - n)
Proof.forall n m : t, n <= m -> S m - n == S (m - n)
intros n m H.n, m:t
H:n <= m
S m - n == S (m - n) rewrite <- (add_1_l m).n, m:t
H:n <= m
1 + m - n == S (m - n) rewrite <- (add_1_l (m - n)).n, m:t
H:n <= m
1 + m - n == 1 + (m - n)
symmetry; now apply add_sub_assoc.
Qed.

Theorem add_sub : forall n m, (n + m) - m == n.forall n m : t, n + m - m == n
Proof.forall n m : t, n + m - m == n
intros n m.n, m:t
n + m - m == n rewrite <- add_sub_assoc by (apply le_refl).n, m:t
n + (m - m) == n
rewrite sub_diag; now rewrite add_0_r.
Qed.

Theorem sub_add : forall n m, n <= m -> (m - n) + n == m.forall n m : t, n <= m -> m - n + n == m
Proof.forall n m : t, n <= m -> m - n + n == m
intros n m H.n, m:t
H:n <= m
m - n + n == m rewrite add_comm.n, m:t
H:n <= m
n + (m - n) == m rewrite add_sub_assoc by assumption.n, m:t
H:n <= m
n + m - n == m
rewrite add_comm.n, m:t
H:n <= m
m + n - n == m apply add_sub.
Qed.

Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.forall n m p : t, m + p == n -> n - m == p
Proof.forall n m p : t, m + p == n -> n - m == p
intros n m p H.n, m, p:t
H:m + p == n
n - m == p symmetry.n, m, p:t
H:m + p == n
p == n - m
assert (H1 : m + p - m == n - m) by now rewrite H.n, m, p:t
H:m + p == n
H1:m + p - m == n - m
p == n - m
rewrite add_comm in H1.n, m, p:t
H:m + p == n
H1:p + m - m == n - m
p == n - m now rewrite add_sub in H1.
Qed.

Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m.forall n m p : t, m + p == n -> n - p == m
Proof.forall n m p : t, m + p == n -> n - p == m
intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l.
Qed.

(* This could be proved by adding m to both sides. Then the proof would
use add_sub_assoc and sub_0_le, which is proven below. *)

Theorem add_sub_eq_nz : forall n m p, p ~= 0 -> n - m == p -> m + p == n.forall n m p : t, p ~= 0 -> n - m == p -> m + p == n
Proof.forall n m p : t, p ~= 0 -> n - m == p -> m + p == n
intros n m p H; double_induct n m.p:t
H:p ~= 0
forall m : t, 0 - m == p -> m + p == 0
p:t
H:p ~= 0
forall n : t, S n - 0 == p -> 0 + p == S n
p:t
H:p ~= 0
forall n m : t,
(n - m == p -> m + p == n) ->
S n - S m == p -> S m + p == S n
intros m H1; rewrite sub_0_l in H1.p:t
H:p ~= 0
m:t
H1:0 == p
m + p == 0
p:t
H:p ~= 0
forall n : t, S n - 0 == p -> 0 + p == S n
p:t
H:p ~= 0
forall n m : t,
(n - m == p -> m + p == n) ->
S n - S m == p -> S m + p == S n symmetry in H1; false_hyp H1 H.p:t
H:p ~= 0
forall n : t, S n - 0 == p -> 0 + p == S n
p:t
H:p ~= 0
forall n m : t,
(n - m == p -> m + p == n) ->
S n - S m == p -> S m + p == S n
intro n; rewrite sub_0_r; now rewrite add_0_l.p:t
H:p ~= 0
forall n m : t,
(n - m == p -> m + p == n) ->
S n - S m == p -> S m + p == S n
intros n m IH H1.p:t
H:p ~= 0
n, m:t
IH:n - m == p -> m + p == n
H1:S n - S m == p
S m + p == S n rewrite sub_succ in H1.p:t
H:p ~= 0
n, m:t
IH:n - m == p -> m + p == n
H1:n - m == p
S m + p == S n apply IH in H1.p:t
H:p ~= 0
n, m:t
IH:n - m == p -> m + p == n
H1:m + p == n
S m + p == S n
rewrite add_succ_l; now rewrite H1.
Qed.

Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.forall n m p : t, n - (m + p) == n - m - p
Proof.forall n m p : t, n - (m + p) == n - m - p
intros n m; induct p.n, m:t
n - (m + 0) == n - m - 0
n, m:t
forall n0 : t,
n - (m + n0) == n - m - n0 ->
n - (m + S n0) == n - m - S n0
rewrite add_0_r; now rewrite sub_0_r.n, m:t
forall n0 : t,
n - (m + n0) == n - m - n0 ->
n - (m + S n0) == n - m - S n0
intros p IH.n, m, p:t
IH:n - (m + p) == n - m - p
n - (m + S p) == n - m - S p rewrite add_succ_r; do 2 rewrite sub_succ_r.n, m, p:t
IH:n - (m + p) == n - m - p
P (n - (m + p)) == P (n - m - p) now rewrite IH.
Qed.

Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m.forall n m p : t, p <= n -> n + m - p == n - p + m
Proof.forall n m p : t, p <= n -> n + m - p == n - p + m
intros n m p H.n, m, p:t
H:p <= n
n + m - p == n - p + m
rewrite (add_comm n m).n, m, p:t
H:p <= n
m + n - p == n - p + m
rewrite <- add_sub_assoc by assumption.n, m, p:t
H:p <= n
m + (n - p) == n - p + m
now rewrite (add_comm m (n - p)).
Qed.

Sub and order

Theorem le_sub_l : forall n m, n - m <= n.forall n m : t, n - m <= n
Proof.forall n m : t, n - m <= n
intro n; induct m.n:t
n - 0 <= n
n:t
forall n0 : t, n - n0 <= n -> n - S n0 <= n
rewrite sub_0_r; now apply eq_le_incl.n:t
forall n0 : t, n - n0 <= n -> n - S n0 <= n
intros m IH.n, m:t
IH:n - m <= n
n - S m <= n rewrite sub_succ_r.n, m:t
IH:n - m <= n
P (n - m) <= n
apply le_trans with (n - m); [apply le_pred_l | assumption].
Qed.

Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m.forall n m : t, n - m == 0 <-> n <= m
Proof.forall n m : t, n - m == 0 <-> n <= m
double_induct n m.forall m : t, 0 - m == 0 <-> 0 <= m
forall n : t, S n - 0 == 0 <-> S n <= 0
forall n m : t,
n - m == 0 <-> n <= m -> S n - S m == 0 <-> S n <= S m
intro m; split; intro; [apply le_0_l | apply sub_0_l].forall n : t, S n - 0 == 0 <-> S n <= 0
forall n m : t,
n - m == 0 <-> n <= m -> S n - S m == 0 <-> S n <= S m
intro m; rewrite sub_0_r; split; intro H;
[false_hyp H neq_succ_0 | false_hyp H nle_succ_0].forall n m : t,
n - m == 0 <-> n <= m -> S n - S m == 0 <-> S n <= S m
intros n m H.n, m:t
H:n - m == 0 <-> n <= m
S n - S m == 0 <-> S n <= S m rewrite <- succ_le_mono.n, m:t
H:n - m == 0 <-> n <= m
S n - S m == 0 <-> n <= m now rewrite sub_succ.
Qed.

Theorem sub_add_le : forall n m, n <= n - m + m.forall n m : t, n <= n - m + m
Proof.forall n m : t, n <= n - m + m
intros.n, m:t
n <= n - m + m
destruct (le_ge_cases n m) as [LE|GE].n, m:t
LE:n <= m
n <= n - m + m
n, m:t
GE:m <= n
n <= n - m + m
rewrite <- sub_0_le in LE.n, m:t
LE:n - m == 0
n <= n - m + m
n, m:t
GE:m <= n
n <= n - m + m rewrite LE; nzsimpl.n, m:t
LE:n - m == 0
n <= m
n, m:t
GE:m <= n
n <= n - m + m
now rewrite <- sub_0_le.n, m:t
GE:m <= n
n <= n - m + m
rewrite sub_add by assumption.n, m:t
GE:m <= n
n <= n apply le_refl.
Qed.

Theorem le_sub_le_add_r : forall n m p,
 n - p <= m <-> n <= m + p.forall n m p : t, n - p <= m <-> n <= m + p
Proof.forall n m p : t, n - p <= m <-> n <= m + p
intros n m p.n, m, p:t
n - p <= m <-> n <= m + p
split; intros LE.n, m, p:t
LE:n - p <= m
n <= m + p
n, m, p:t
LE:n <= m + p
n - p <= m
rewrite (add_le_mono_r _ _ p) in LE.n, m, p:t
LE:n - p + p <= m + p
n <= m + p
n, m, p:t
LE:n <= m + p
n - p <= m
apply le_trans with (n-p+p); auto using sub_add_le.n, m, p:t
LE:n <= m + p
n - p <= m
destruct (le_ge_cases n p) as [LE'|GE].n, m, p:t
LE:n <= m + p
LE':n <= p
n - p <= m
n, m, p:t
LE:n <= m + p
GE:p <= n
n - p <= m
rewrite <- sub_0_le in LE'.n, m, p:t
LE:n <= m + p
LE':n - p == 0
n - p <= m
n, m, p:t
LE:n <= m + p
GE:p <= n
n - p <= m rewrite LE'.n, m, p:t
LE:n <= m + p
LE':n - p == 0
0 <= m
n, m, p:t
LE:n <= m + p
GE:p <= n
n - p <= m apply le_0_l.n, m, p:t
LE:n <= m + p
GE:p <= n
n - p <= m
rewrite (add_le_mono_r _ _ p).n, m, p:t
LE:n <= m + p
GE:p <= n
n - p + p <= m + p now rewrite sub_add.
Qed.

Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p.forall n m p : t, n - m <= p <-> n <= m + p
Proof.forall n m p : t, n - m <= p <-> n <= m + p
intros n m p.n, m, p:t
n - m <= p <-> n <= m + p rewrite add_comm; apply le_sub_le_add_r.
Qed.

Theorem lt_sub_lt_add_r : forall n m p,
 n - p < m -> n < m + p.forall n m p : t, n - p < m -> n < m + p
Proof.forall n m p : t, n - p < m -> n < m + p
intros n m p LT.n, m, p:t
LT:n - p < m
n < m + p
rewrite (add_lt_mono_r _ _ p) in LT.n, m, p:t
LT:n - p + p < m + p
n < m + p
apply le_lt_trans with (n-p+p); auto using sub_add_le.
Qed.

Unfortunately, we do not have n < m + p → n - p < m. For instance 1<0+2 but not 1-2<0.

Theorem lt_sub_lt_add_l : forall n m p, n - m < p -> n < m + p.forall n m p : t, n - m < p -> n < m + p
Proof.forall n m p : t, n - m < p -> n < m + p
intros n m p.n, m, p:t
n - m < p -> n < m + p rewrite add_comm; apply lt_sub_lt_add_r.
Qed.

Theorem le_add_le_sub_r : forall n m p, n + p <= m -> n <= m - p.forall n m p : t, n + p <= m -> n <= m - p
Proof.forall n m p : t, n + p <= m -> n <= m - p
intros n m p LE.n, m, p:t
LE:n + p <= m
n <= m - p
apply (add_le_mono_r _ _ p).n, m, p:t
LE:n + p <= m
n + p <= m - p + p
rewrite sub_add.n, m, p:t
LE:n + p <= m
n + p <= m
n, m, p:t
LE:n + p <= m
p <= m assumption.n, m, p:t
LE:n + p <= m
p <= m
apply le_trans with (n+p); trivial.n, m, p:t
LE:n + p <= m
p <= n + p
rewrite <- (add_0_l p) at 1.n, m, p:t
LE:n + p <= m
0 + p <= n + p rewrite <- add_le_mono_r.n, m, p:t
LE:n + p <= m
0 <= n apply le_0_l.
Qed.

Unfortunately, we do not have n ≤ m - p → n + p ≤ m. For instance 0<=1-2 but not 2+0<=1.

Theorem le_add_le_sub_l : forall n m p, n + p <= m -> p <= m - n.forall n m p : t, n + p <= m -> p <= m - n
Proof.forall n m p : t, n + p <= m -> p <= m - n
intros n m p.n, m, p:t
n + p <= m -> p <= m - n rewrite add_comm; apply le_add_le_sub_r.
Qed.

Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.forall n m p : t, n + p < m <-> n < m - p
Proof.forall n m p : t, n + p < m <-> n < m - p
intros n m p.n, m, p:t
n + p < m <-> n < m - p
destruct (le_ge_cases p m) as [LE|GE].n, m, p:t
LE:p <= m
n + p < m <-> n < m - p
n, m, p:t
GE:m <= p
n + p < m <-> n < m - p
rewrite <- (sub_add p m) at 1 by assumption.n, m, p:t
LE:p <= m
n + p < m - p + p <-> n < m - p
n, m, p:t
GE:m <= p
n + p < m <-> n < m - p
now rewrite <- add_lt_mono_r.n, m, p:t
GE:m <= p
n + p < m <-> n < m - p
assert (GE' := GE).n, m, p:t
GE, GE':m <= p
n + p < m <-> n < m - p rewrite <- sub_0_le in GE'; rewrite GE'.n, m, p:t
GE:m <= p
GE':m - p == 0
n + p < m <-> n < 0
split; intros LT.n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n + p < m
n < 0
n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n < 0
n + p < m
elim (lt_irrefl m).n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n + p < m
m < m
n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n < 0
n + p < m apply le_lt_trans with (n+p); trivial.n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n + p < m
m <= n + p
n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n < 0
n + p < m
 rewrite <- (add_0_l m).n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n + p < m
0 + m <= n + p
n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n < 0
n + p < m apply add_le_mono.n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n + p < m
0 <= n
n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n + p < m
m <= p
n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n < 0
n + p < m apply le_0_l.n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n + p < m
m <= p
n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n < 0
n + p < m assumption.n, m, p:t
GE:m <= p
GE':m - p == 0
LT:n < 0
n + p < m
now elim (nlt_0_r n).
Qed.

Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n.forall n m p : t, n + p < m <-> p < m - n
Proof.forall n m p : t, n + p < m <-> p < m - n
intros n m p.n, m, p:t
n + p < m <-> p < m - n rewrite add_comm; apply lt_add_lt_sub_r.
Qed.

Theorem sub_lt : forall n m, m <= n -> 0 < m -> n - m < n.forall n m : t, m <= n -> 0 < m -> n - m < n
Proof.forall n m : t, m <= n -> 0 < m -> n - m < n
intros n m LE LT.n, m:t
LE:m <= n
LT:0 < m
n - m < n
assert (LE' := le_sub_l n m).n, m:t
LE:m <= n
LT:0 < m
LE':n - m <= n
n - m < n rewrite lt_eq_cases in LE'.n, m:t
LE:m <= n
LT:0 < m
LE':n - m < n \/ n - m == n
n - m < n
destruct LE' as [LT'|EQ].n, m:t
LE:m <= n
LT:0 < m
LT':n - m < n
n - m < n
n, m:t
LE:m <= n
LT:0 < m
EQ:n - m == n
n - m < n assumption.n, m:t
LE:m <= n
LT:0 < m
EQ:n - m == n
n - m < n
apply add_sub_eq_nz in EQ; [|order].n, m:t
LE:m <= n
LT:0 < m
EQ:m + n == n
n - m < n
rewrite (add_lt_mono_r _ _ n), add_0_l in LT.n, m:t
LE:m <= n
LT:n < m + n
EQ:m + n == n
n - m < n order.
Qed.

Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p.forall n m p : t, n <= m -> n - p <= m - p
Proof.forall n m p : t, n <= m -> n - p <= m - p
 intros.n, m, p:t
H:n <= m
n - p <= m - p rewrite le_sub_le_add_r.n, m, p:t
H:n <= m
n <= m - p + p transitivity m.n, m, p:t
H:n <= m
n <= m
n, m, p:t
H:n <= m
m <= m - p + p assumption.n, m, p:t
H:n <= m
m <= m - p + p apply sub_add_le.
Qed.

Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n.forall n m p : t, n <= m -> p - m <= p - n
Proof.forall n m p : t, n <= m -> p - m <= p - n
 intros.n, m, p:t
H:n <= m
p - m <= p - n rewrite le_sub_le_add_r.n, m, p:t
H:n <= m
p <= p - n + m
 transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l].
Qed.

Sub and mul

Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.forall n m : t, n * P m == n * m - n
Proof.forall n m : t, n * P m == n * m - n
intros n m; cases m.n:t
n * P 0 == n * 0 - n
n:t
forall n0 : t, n * P (S n0) == n * S n0 - n
now rewrite pred_0, mul_0_r, sub_0_l.n:t
forall n0 : t, n * P (S n0) == n * S n0 - n
intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc.n, m:t
n * m == n * m + (n - n)
n, m:t
n <= n
now rewrite sub_diag, add_0_r.n, m:t
n <= n
now apply eq_le_incl.
Qed.

Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.forall n m p : t, (n - m) * p == n * p - m * p
Proof.forall n m p : t, (n - m) * p == n * p - m * p
intros n m p; induct n.m, p:t
(0 - m) * p == 0 * p - m * p
m, p:t
forall n : t,
(n - m) * p == n * p - m * p ->
(S n - m) * p == S n * p - m * p
now rewrite sub_0_l, mul_0_l, sub_0_l.m, p:t
forall n : t,
(n - m) * p == n * p - m * p ->
(S n - m) * p == S n * p - m * p
intros n IH.m, p, n:t
IH:(n - m) * p == n * p - m * p
(S n - m) * p == S n * p - m * p destruct (le_gt_cases m n) as [H | H].m, p, n:t
IH:(n - m) * p == n * p - m * p
H:m <= n
(S n - m) * p == S n * p - m * p
m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
(S n - m) * p == S n * p - m * p
rewrite sub_succ_l by assumption.m, p, n:t
IH:(n - m) * p == n * p - m * p
H:m <= n
S (n - m) * p == S n * p - m * p
m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
(S n - m) * p == S n * p - m * p do 2 rewrite mul_succ_l.m, p, n:t
IH:(n - m) * p == n * p - m * p
H:m <= n
(n - m) * p + p == n * p + p - m * p
m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
(S n - m) * p == S n * p - m * p
rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p).m, p, n:t
IH:(n - m) * p == n * p - m * p
H:m <= n
p + (n - m) * p == p + n * p - m * p
m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
(S n - m) * p == S n * p - m * p
rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r.m, p, n:t
IH:(n - m) * p == n * p - m * p
H:m <= n
p + (n - m) * p == p + (n * p - m * p)
m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
(S n - m) * p == S n * p - m * p
now apply add_cancel_l.m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
(S n - m) * p == S n * p - m * p
assert (H1 : S n <= m); [now apply le_succ_l |].m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
H1:S n <= m
(S n - m) * p == S n * p - m * p
setoid_replace (S n - m) with 0 by now apply sub_0_le.m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
H1:S n <= m
0 * p == S n * p - m * p
setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r).m, p, n:t
IH:(n - m) * p == n * p - m * p
H:n < m
H1:S n <= m
0 * p == 0
apply mul_0_l.
Qed.

Theorem mul_sub_distr_l : forall n m p, p * (n - m) == p * n - p * m.forall n m p : t, p * (n - m) == p * n - p * m
Proof.forall n m p : t, p * (n - m) == p * n - p * m
intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m).n, m, p:t
(n - m) * p == n * p - m * p
apply mul_sub_distr_r.
Qed.

Alternative definitions of ≤ and < based on +

Definition le_alt n m := exists p, p + n == m.
Definition lt_alt n m := exists p, S p + n == m.

Lemma le_equiv : forall n m, le_alt n m <-> n <= m.forall n m : t, le_alt n m <-> n <= m
Proof.forall n m : t, le_alt n m <-> n <= m
split.n, m:t
le_alt n m -> n <= m
n, m:t
n <= m -> le_alt n m
intros (p,H).n, m, p:t
H:p + n == m
n <= m
n, m:t
n <= m -> le_alt n m rewrite <- H, add_comm.n, m, p:t
H:p + n == m
n <= n + p
n, m:t
n <= m -> le_alt n m apply le_add_r.n, m:t
n <= m -> le_alt n m
intro H.n, m:t
H:n <= m
le_alt n m exists (m-n).n, m:t
H:n <= m
m - n + n == m now apply sub_add.
Qed.

Lemma lt_equiv : forall n m, lt_alt n m <-> n < m.forall n m : t, lt_alt n m <-> n < m
Proof.forall n m : t, lt_alt n m <-> n < m
split.n, m:t
lt_alt n m -> n < m
n, m:t
n < m -> lt_alt n m
intros (p,H).n, m, p:t
H:S p + n == m
n < m
n, m:t
n < m -> lt_alt n m rewrite <- H, add_succ_l, lt_succ_r, add_comm.n, m, p:t
H:S p + n == m
n <= n + p
n, m:t
n < m -> lt_alt n m apply le_add_r.n, m:t
n < m -> lt_alt n m
intro H.n, m:t
H:n < m
lt_alt n m exists (m-S n).n, m:t
H:n < m
S (m - S n) + n == m rewrite add_succ_l, <- add_succ_r.n, m:t
H:n < m
m - S n + S n == m
apply sub_add.n, m:t
H:n < m
S n <= m now rewrite le_succ_l.
Qed.

Instance le_alt_wd : Proper (eq==>eq==>iff) le_alt.Proper (eq ==> eq ==> iff) le_alt
Proof.Proper (eq ==> eq ==> iff) le_alt
 intros x x' Hx y y' Hy; unfold le_alt.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, p + x == y) <->
(exists p : t, p + x' == y')
 setoid_rewrite Hx.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, p + x' == y) <->
(exists p : t, p + x' == y') setoid_rewrite Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, p + x' == y') <->
(exists p : t, p + x' == y') auto with *.
Qed.

Instance lt_alt_wd : Proper (eq==>eq==>iff) lt_alt.Proper (eq ==> eq ==> iff) lt_alt
Proof.Proper (eq ==> eq ==> iff) lt_alt
 intros x x' Hx y y' Hy; unfold lt_alt.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, S p + x == y) <->
(exists p : t, S p + x' == y')
 setoid_rewrite Hx.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, S p + x' == y) <->
(exists p : t, S p + x' == y') setoid_rewrite Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, S p + x' == y') <->
(exists p : t, S p + x' == y') auto with *.
Qed.

With these alternative definition, the dichotomy:

∀ n m, n ≤ m ∨ m ≤ n

becomes:

∀ n m, (∃ p, p + n == m) ∨ (∃ p, p + m == n)

We will need this in the proof of induction principle for integers constructed as pairs of natural numbers. This formula can be proved from know properties of ≤. However, it can also be done directly.

Theorem le_alt_dichotomy : forall n m, le_alt n m \/ le_alt m n.forall n m : t, le_alt n m \/ le_alt m n
Proof.forall n m : t, le_alt n m \/ le_alt m n
intros n m; induct n.m:t
le_alt 0 m \/ le_alt m 0
m:t
forall n : t,
le_alt n m \/ le_alt m n ->
le_alt (S n) m \/ le_alt m (S n)
left; exists m; apply add_0_r.m:t
forall n : t,
le_alt n m \/ le_alt m n ->
le_alt (S n) m \/ le_alt m (S n)
intros n IH.m, n:t
IH:le_alt n m \/ le_alt m n
le_alt (S n) m \/ le_alt m (S n)
destruct IH as [[p H] | [p H]].m, n, p:t
H:p + n == m
le_alt (S n) m \/ le_alt m (S n)
m, n, p:t
H:p + m == n
le_alt (S n) m \/ le_alt m (S n)
destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.m, n, p:t
H:0 + n == m
H1:p == 0
le_alt (S n) m \/ le_alt m (S n)
m, n, p, p':t
H:S p' + n == m
H1:p == S p'
le_alt (S n) m \/ le_alt m (S n)
m, n, p:t
H:p + m == n
le_alt (S n) m \/ le_alt m (S n)
rewrite add_0_l in H.m, n, p:t
H:n == m
H1:p == 0
le_alt (S n) m \/ le_alt m (S n)
m, n, p, p':t
H:S p' + n == m
H1:p == S p'
le_alt (S n) m \/ le_alt m (S n)
m, n, p:t
H:p + m == n
le_alt (S n) m \/ le_alt m (S n) right; exists (S 0); rewrite H, add_succ_l;
 now rewrite add_0_l.m, n, p, p':t
H:S p' + n == m
H1:p == S p'
le_alt (S n) m \/ le_alt m (S n)
m, n, p:t
H:p + m == n
le_alt (S n) m \/ le_alt m (S n)
left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H.m, n, p:t
H:p + m == n
le_alt (S n) m \/ le_alt m (S n)
right; exists (S p).m, n, p:t
H:p + m == n
S p + m == S n rewrite add_succ_l; now rewrite H.
Qed.

Theorem add_dichotomy :
  forall n m, (exists p, p + n == m) \/ (exists p, p + m == n).forall n m : t,
(exists p : t, p + n == m) \/
(exists p : t, p + m == n)
Proof.forall n m : t,
(exists p : t, p + n == m) \/
(exists p : t, p + m == n) exact le_alt_dichotomy. Qed.

End NSubProp.