Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core.

Local Set Universe Minimization ToSet.

Local Close Scope trunc_scope.
Local Open Scope nat_scope.

Ltac nat_absurd_trivial :=
  unfold ">" in *; unfold "<" in *;
  match goal with
  | [ H : ?n.+1 <= 0 |- _ ] => contradiction (not_leq_Sn_0 n H)
  | [ H : ?n.+1 <= ?n |- _ ] => contradiction (not_lt_n_n n H)
  | [ H1 : ?k.+1 <= ?n |- _ ] =>
      match goal with
      | [ H2 : ?n <= ?k |- _] =>
          contradiction (not_leq_Sn_n k (@leq_trans _ _ _ H1 H2))
      end
  end.

#[export] Hint Resolve not_lt_n_n : nat.
#[export] Hint Resolve not_lt_n_0 : nat.
#[export] Hint Resolve not_leq_Sn_0 : nat.
#[export] Hint Extern 2 => nat_absurd_trivial : nat.

(** This is defined so that it can be added to the [nat] auto hint database. *)
Local Definition symmetric_paths_nat (n m : nat)
  : n = m -> m = n := @symmetric_paths nat n m.

Local Definition transitive_paths_nat (n m k : nat)
  : n = m -> m = k -> n = k := @transitive_paths nat n m k.

#[export] Hint Resolve symmetric_paths_nat | 5 : nat.
#[export] Hint Resolve transitive_paths_nat : nat.
#[export] Hint Resolve leq_0_n : nat.
#[export] Hint Resolve leq_trans : nat.
#[export] Hint Resolve leq_antisym : nat.

Proposition assoc_nat_add (n m k : nat)
  : n + (m + k) = (n + m) + k.
n, m, k: nat
n + (m + k) = n + m + k
Proof.
n, m, k: nat
n + (m + k) = n + m + k
  revert m k; simple_induction n n IHn.
forall m k : nat, 0 + (m + k) = 0 + m + k
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
forall m k : nat, n.+1 + (m + k) = n.+1 + m + k
  -
forall m k : nat, 0 + (m + k) = 0 + m + k reflexivity.
  -
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
forall m k : nat, n.+1 + (m + k) = n.+1 + m + k intros m k.
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
m, k: nat
n.+1 + (m + k) = n.+1 + m + k change (n.+1 + (m + k)) with (n + (m + k)).+1.
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
m, k: nat
(n + (m + k)).+1 = n.+1 + m + k
    apply (transitive_paths _ _ _ (nat_add_n_Sm _ _)).
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
m, k: nat
n + (m + k).+1 = n.+1 + m + k
    change (m + k).+1 with (m.+1 + k);
    change (n.+1 + m) with (n + m).+1.
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
m, k: nat
n + (m.+1 + k) = (n + m).+1 + k
    apply (transitive_paths _ _ _ (IHn m.+1 k)).
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
m, k: nat
n + m.+1 + k = (n + m).+1 + k
    apply (ap (fun zz => zz + k)).
n: nat
IHn: forall m k : nat, n + (m + k) = n + m + k
m, k: nat
n + m.+1 = (n + m).+1
    apply symmetric_paths, nat_add_n_Sm. 
Defined.

Proposition not_lt_implies_geq {n m : nat} : ~(n < m) -> m <= n.
n, m: nat
~ (n < m) -> m <= n
Proof.
n, m: nat
~ (n < m) -> m <= n
  intros not_lt.
n, m: nat
not_lt: ~ (n < m)
m <= n
  destruct (@leq_dichot m n); [ assumption | contradiction].
Defined.

Proposition not_leq_implies_gt {n m : nat} : ~(n <= m) -> m < n.
n, m: nat
~ (n <= m) -> m < n
Proof.
n, m: nat
~ (n <= m) -> m < n
  intros not_leq.
n, m: nat
not_leq: ~ (n <= m)
m < n 
  destruct (@leq_dichot n m); [ contradiction | assumption].
Defined.

Proposition lt_implies_not_geq {n m : nat} : (n < m) -> ~(m <= n).
n, m: nat
n < m -> ~ (m <= n)
Proof.
n, m: nat
n < m -> ~ (m <= n)
  intros ineq1 ineq2.
n, m: nat
ineq1: n < m
ineq2: m <= n
Empty
  contradiction (not_lt_n_n n).
n, m: nat
ineq1: n < m
ineq2: m <= n
n < n by apply (leq_trans ineq1).
Defined.

Proposition leq_implies_not_gt {n m : nat} : (n <= m) -> ~(m < n).
n, m: nat
n <= m -> ~ (m < n)
Proof.
n, m: nat
n <= m -> ~ (m < n)
  intros ineq1 ineq2.
n, m: nat
ineq1: n <= m
ineq2: m < n
Empty
  contradiction (not_lt_n_n n); by refine (leq_trans _ ineq2).
Defined.

Ltac convert_to_positive :=
  match goal with
  | [ H : ~ (?n < ?m) |- _] =>  apply not_lt_implies_geq in H
  | [ H : ~ (?n <= ?m) |- _] => apply not_leq_implies_gt in H
  | [|- ~ (?n < ?m) ] => apply leq_implies_not_gt
  | [|- ~ (?n <= ?m) ] => apply lt_implies_not_geq
  end.

#[export] Hint Extern 2 => convert_to_positive : nat.

(** Because of the inductive definition of [<=], one can destruct the proof of [n <= m] and get a judgemental identification between [n] and [m] rather than a propositional one, which may be preferable to the following lemma. *)
Proposition leq_split {n m : nat} : (n <= m) -> sum (n < m) (n = m).
n, m: nat
n <= m -> ((n < m) + (n = m))%type
Proof.
n, m: nat
n <= m -> ((n < m) + (n = m))%type
  intro l.
n, m: nat
l: n <= m
((n < m) + (n = m))%type induction l.
n: nat
((n < n) + (n = n))%type
n, m: nat
l: n <= m
IHl: ((n < m) + (n = m))%type
((n < m.+1) + (n = m.+1))%type
  -
n: nat
((n < n) + (n = n))%type now right.
  -
n, m: nat
l: n <= m
IHl: ((n < m) + (n = m))%type
((n < m.+1) + (n = m.+1))%type left.
n, m: nat
l: n <= m
IHl: ((n < m) + (n = m))%type
n < m.+1 exact (leq_S_n' _ _ l).
Defined.

Proposition diseq_implies_lt (n m : nat)
  : n <> m -> sum (n < m) (n > m).
n, m: nat
n <> m -> ((n < m) + (n > m))%type
Proof.
n, m: nat
n <> m -> ((n < m) + (n > m))%type
  intros diseq.
n, m: nat
diseq: n <> m
((n < m) + (n > m))%type
  destruct (dec (n < m)) as [| a]; [ now left |].
n, m: nat
diseq: n <> m
a: ~ (n < m)
((n < m) + (n > m))%type
  right.
n, m: nat
diseq: n <> m
a: ~ (n < m)
n > m destruct (@leq_dichot n m) as [n_leq_m | gt];
    [ | assumption].
n, m: nat
diseq: n <> m
a: ~ (n < m)
n_leq_m: n <= m
n > m
  destruct n_leq_m;
    [ now contradiction diseq
    | contradiction a; now apply leq_S_n'].
Defined.

Proposition lt_implies_diseq (n m : nat)
  : n < m -> (n <> m).
n, m: nat
n < m -> n <> m
Proof.
n, m: nat
n < m -> n <> m
  intros ineq eq.
n, m: nat
ineq: n < m
eq: n = m
Empty rewrite eq in ineq.
n, m: nat
ineq: m < m
eq: n = m
Empty
  contradiction (not_lt_n_n m).
Defined.

#[export] Hint Resolve lt_implies_diseq : nat.

(** This lemma is just for convenience in the case where the user forgets to unfold the definition of [<]. *)
Proposition n_lt_Sn (n : nat) : n < n.+1.
n: nat
n < n.+1
Proof.
n: nat
n < n.+1
  exact (leq_n n.+1).
Defined.

Proposition leq_S' (n m : nat) : n.+1 <= m -> n <= m.
n, m: nat
n.+1 <= m -> n <= m
Proof.
n, m: nat
n.+1 <= m -> n <= m
  intro l.
n, m: nat
l: n.+1 <= m
n <= m
  now apply leq_S_n, leq_S.
Defined.

Ltac easy_eq_to_ineq :=
  match goal with
  | [ H : ?x = ?n    |- ?x <= ?n ] => destruct H; constructor
  | [ H : ?x.+1 = ?n |- ?x <= ?n ] => rewrite <- H; constructor;
                                      constructor
  | [ H : ?x.+1 = ?n |- ?x < ?n  ] => rewrite <- H; apply leq_n
  | [ H : ?x.+2 = ?n |- ?x <= ?n ] => rewrite <- H; apply leq_S';
                                      apply leq_S'; apply leq_n
  | [ H : ?x.+2 = ?n |- ?x < ?n ] => rewrite <- H; apply leq_S_n';
                                      apply leq_S
  end.

#[export] Hint Extern 3 => easy_eq_to_ineq : nat.

Proposition mixed_trans1 (n m k : nat)
  : n <= m -> m < k -> n < k.
n, m, k: nat
n <= m -> m < k -> n < k
Proof.
n, m, k: nat
n <= m -> m < k -> n < k
  intros l j.
n, m, k: nat
l: n <= m
j: m < k
n < k apply leq_S_n' in l.
n, m, k: nat
l: n.+1 <= m.+1
j: m < k
n < k
  apply (@leq_trans (n.+1) (m.+1) k); trivial. 
Defined.

Ltac leq_trans_resolve :=
  match goal with
  | [ H : ?n <= ?m |- ?n <= ?k ] => apply (leq_trans H)
  | [ H : ?k <= ?m |- ?n <= ?k ] => refine (leq_trans _ H)
  | [ H : ?n <= ?m |- ?n < ?k ] => apply (mixed_trans1 _ _ _ H)
  | [ H : ?m <= ?k |- ?n < ?k ] => refine (leq_trans _ H)
  | [ H : ?m <  ?k |- ?n < ?k ] => refine (mixed_trans1 _ _ _ _ H)
  | [ H : ?n <  ?m |- ?n < ?k ] => apply (leq_trans H)
  end.

#[export] Hint Extern 2 => leq_trans_resolve : nat.

Proposition mixed_trans2 (n m k : nat)
  : n < m -> m <= k -> n < k.
n, m, k: nat
n < m -> m <= k -> n < k
Proof.
n, m, k: nat
n < m -> m <= k -> n < k
  intros l j.
n, m, k: nat
l: n < m
j: m <= k
n < k apply (@leq_trans (n.+1) m k); trivial. 
Defined.

#[export] Hint Resolve mixed_trans1 : nat.
#[export] Hint Resolve mixed_trans2 : nat.

Proposition sub_n_n (n : nat) : n - n = 0.
n: nat
n - n = 0
Proof.
n: nat
n - n = 0
  simple_induction n n IHn.
0 - 0 = 0
n: nat
IHn: n - n = 0
n.+1 - n.+1 = 0
  -
0 - 0 = 0 reflexivity.
  -
n: nat
IHn: n - n = 0
n.+1 - n.+1 = 0 simpl; exact IHn.
Defined.

Proposition sub_n_0 (n : nat) : n - 0 = n.
n: nat
n - 0 = n
Proof.
n: nat
n - 0 = n
 destruct n; reflexivity.
Defined.

Ltac rewrite_subn0 :=
  match goal with
  | [ |- context [ ?n - 0 ] ] => rewrite -> sub_n_0
  end.

Ltac rewrite_subnn :=
  match goal with
  | [ |- context [ ?n - ?n ] ] => rewrite -> sub_n_n
  end.

#[export] Hint Rewrite -> sub_n_0 : nat.
#[export] Hint Rewrite -> sub_n_n : nat.
#[export] Hint Resolve sub_n_0 : nat.

Proposition add_n_sub_n_eq (m n : nat) : m + n - n = m.
m, n: nat
m + n - n = m
Proof.
m, n: nat
m + n - n = m
  destruct m.
n: nat
0 + n - n = 0
m, n: nat
m.+1 + n - n = m.+1
  -
n: nat
0 + n - n = 0 simple_induction' n.
0 + 0 - 0 = 0
n: nat
IH: 0 + n - n = 0
0 + n.+1 - n.+1 = 0
    +
0 + 0 - 0 = 0 reflexivity.
    +
n: nat
IH: 0 + n - n = 0
0 + n.+1 - n.+1 = 0 assumption.
  -
m, n: nat
m.+1 + n - n = m.+1 simple_induction' n.
m: nat
m.+1 + 0 - 0 = m.+1
m, n: nat
IH: m.+1 + n - n = m.+1
m.+1 + n.+1 - n.+1 = m.+1
    +
m: nat
m.+1 + 0 - 0 = m.+1 simpl.
m: nat
(m + 0).+1 = m.+1 destruct (add_n_O m); reflexivity.
    +
m, n: nat
IH: m.+1 + n - n = m.+1
m.+1 + n.+1 - n.+1 = m.+1 simpl.
m, n: nat
IH: m.+1 + n - n = m.+1
m + n.+1 - n = m.+1 destruct (add_n_Sm m n).
m, n: nat
IH: m.+1 + n - n = m.+1
(m + n).+1 - n = m.+1 assumption.
Defined.

Proposition add_n_sub_n_eq' (m n : nat) : n + m - n = m.
m, n: nat
n + m - n = m
Proof.
m, n: nat
n + m - n = m 
  destruct (nat_add_comm m n).
m, n: nat
m + n - n = m exact (add_n_sub_n_eq m n).
Defined.

Lemma summand_is_sub k m n (p : k + n = m) : k = m - n.
k, m, n: nat
p: k + n = m
k = m - n
Proof.
k, m, n: nat
p: k + n = m
k = m - n
  destruct p.
k, n: nat
k = k + n - n
  symmetry.
k, n: nat
k + n - n = k
  apply add_n_sub_n_eq.
Defined.

Proposition n_lt_m_n_leq_m { n m : nat } : n < m -> n <= m.
n, m: nat
n < m -> n <= m
Proof.
n, m: nat
n < m -> n <= m
  intro H.
n, m: nat
H: n < m
n <= m apply leq_S, leq_S_n in H; exact H.
Defined.

#[export] Hint Resolve n_lt_m_n_leq_m : nat.

Proposition lt_trans (n m k : nat) : n < m -> m < k -> n < k.
n, m, k: nat
n < m -> m < k -> n < k
Proof.
n, m, k: nat
n < m -> m < k -> n < k
  eauto with nat.
Defined.

Proposition not_both_less (n m : nat) : n < m -> ~(m < n).
n, m: nat
n < m -> ~ (m < n)
Proof.
n, m: nat
n < m -> ~ (m < n)
  intros l a; contradiction (not_lt_n_n _ (lt_trans _ _ _ l a)).
Defined.  

Proposition n_leq_add_n_k (n m : nat) : n <= n + m.
n, m: nat
n <= n + m
Proof.
n, m: nat
n <= n + m
  simple_induction n n IHn.
m: nat
0 <= 0 + m
m, n: nat
IHn: n <= n + m
n.+1 <= n.+1 + m
  -
m: nat
0 <= 0 + m apply leq_0_n.
  -
m, n: nat
IHn: n <= n + m
n.+1 <= n.+1 + m simpl; apply leq_S_n', IHn.
Defined.

Proposition n_leq_add_n_k' (n m : nat) : n <= m + n.
n, m: nat
n <= m + n
Proof.
n, m: nat
n <= m + n
  simple_induction' m.
n: nat
n <= 0 + n
n, m: nat
IH: n <= m + n
n <= m.+1 + n
  -
n: nat
n <= 0 + n exact(leq_n n).
  -
n, m: nat
IH: n <= m + n
n <= m.+1 + n simpl.
n, m: nat
IH: n <= m + n
n <= (m + n).+1 apply leq_S.
n, m: nat
IH: n <= m + n
n <= m + n assumption.
Defined.

Proposition natineq0eq0 {n : nat} : n <= 0 -> n = 0.
n: nat
n <= 0 -> n = 0
Proof.
n: nat
n <= 0 -> n = 0
  destruct n.
0 <= 0 -> 0 = 0
n: nat
n.+1 <= 0 -> n.+1 = 0
  -
0 <= 0 -> 0 = 0 reflexivity.
  -
n: nat
n.+1 <= 0 -> n.+1 = 0 intro.
n: nat
H: n.+1 <= 0
n.+1 = 0 contradiction (not_leq_Sn_0 n).
Defined.

Proposition subsubadd (n m k : nat) : n - (m + k) = n - m - k.
n, m, k: nat
n - (m + k) = n - m - k
Proof.
n, m, k: nat
n - (m + k) = n - m - k
  revert m k; simple_induction n n IHn.
forall m k : nat, 0 - (m + k) = 0 - m - k
n: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
forall m k : nat, n.+1 - (m + k) = n.+1 - m - k
  -
forall m k : nat, 0 - (m + k) = 0 - m - k reflexivity.
  -
n: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
forall m k : nat, n.+1 - (m + k) = n.+1 - m - k intro m; destruct m; intro k.
n: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
k: nat
n.+1 - (0 + k) = n.+1 - 0 - k
n: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
m, k: nat
n.+1 - (m.+1 + k) = n.+1 - m.+1 - k
    +
n: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
k: nat
n.+1 - (0 + k) = n.+1 - 0 - k change (0 + k) with k; reflexivity.
    +
n: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
m, k: nat
n.+1 - (m.+1 + k) = n.+1 - m.+1 - k change (m.+1 + k) with (m + k).+1; apply IHn.
Defined.

#[export] Hint Resolve subsubadd : nat.

Proposition subsubadd' (n m k : nat) : n - m - k = n - (m + k).
n, m, k: nat
n - m - k = n - (m + k)
Proof.
n, m, k: nat
n - m - k = n - (m + k)
  auto with nat.
Defined.

Definition nleqSm_dichot {n m : nat}
  : (n <= m.+1) -> sum (n <= m) (n = m.+1).
n, m: nat
n <= m.+1 -> ((n <= m) + (n = m.+1))%type
Proof.
n, m: nat
n <= m.+1 -> ((n <= m) + (n = m.+1))%type
  revert m; simple_induction n n IHn.
forall m : nat,
0 <= m.+1 -> ((0 <= m) + (0 = m.+1))%type
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
forall m : nat,
n.+1 <= m.+1 -> ((n.+1 <= m) + (n.+1 = m.+1))%type
  -
forall m : nat,
0 <= m.+1 -> ((0 <= m) + (0 = m.+1))%type intro.
m: nat
0 <= m.+1 -> ((0 <= m) + (0 = m.+1))%type left.
m: nat
H: 0 <= m.+1
0 <= m exact (leq_0_n m).
  -
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
forall m : nat,
n.+1 <= m.+1 -> ((n.+1 <= m) + (n.+1 = m.+1))%type destruct m.
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
n.+1 <= 1 -> ((n.+1 <= 0) + (n.+1 = 1))%type
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
n.+1 <= m.+2 -> ((n.+1 <= m.+1) + (n.+1 = m.+2))%type
    +
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
n.+1 <= 1 -> ((n.+1 <= 0) + (n.+1 = 1))%type intro l.
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
l: n.+1 <= 1
((n.+1 <= 0) + (n.+1 = 1))%type apply leq_S_n, natineq0eq0 in l.
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
l: n = 0
((n.+1 <= 0) + (n.+1 = 1))%type
      right; apply ap; exact l.
    +
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
n.+1 <= m.+2 -> ((n.+1 <= m.+1) + (n.+1 = m.+2))%type intro l.
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
l: n.+1 <= m.+2
((n.+1 <= m.+1) + (n.+1 = m.+2))%type apply leq_S_n, IHn in l; destruct l as [a | b].
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
a: n <= m
((n.+1 <= m.+1) + (n.+1 = m.+2))%type
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
b: n = m.+1
((n.+1 <= m.+1) + (n.+1 = m.+2))%type
      *
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
a: n <= m
((n.+1 <= m.+1) + (n.+1 = m.+2))%type left.
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
a: n <= m
n.+1 <= m.+1 apply leq_S_n'; exact a.
      *
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
b: n = m.+1
((n.+1 <= m.+1) + (n.+1 = m.+2))%type right.
n: nat
IHn: forall m : nat, n <= m.+1 -> ((n <= m) + (n = m.+1))%type
m: nat
b: n = m.+1
n.+1 = m.+2 apply ap; exact b.
Defined.

Proposition sub_leq_0 (n m : nat) : n <= m -> n - m = 0.
n, m: nat
n <= m -> n - m = 0
Proof.
n, m: nat
n <= m -> n - m = 0
  intro l; induction l.
n: nat
n - n = 0
n, m: nat
l: n <= m
IHl: n - m = 0
n - m.+1 = 0
  -
n: nat
n - n = 0 exact (sub_n_n n).
  -
n, m: nat
l: n <= m
IHl: n - m = 0
n - m.+1 = 0 change (m.+1) with (1 + m).
n, m: nat
l: n <= m
IHl: n - m = 0
n - (1 + m) = 0 destruct n.
m: nat
l: 0 <= m
IHl: 0 - m = 0
0 - (1 + m) = 0
n, m: nat
l: n.+1 <= m
IHl: n.+1 - m = 0
n.+1 - (1 + m) = 0
    +
m: nat
l: 0 <= m
IHl: 0 - m = 0
0 - (1 + m) = 0 reflexivity.
    +
n, m: nat
l: n.+1 <= m
IHl: n.+1 - m = 0
n.+1 - (1 + m) = 0 destruct (nat_add_comm m 1).
n, m: nat
l: n.+1 <= m
IHl: n.+1 - m = 0
n.+1 - (m + 1) = 0
      destruct (symmetric_paths _ _ (subsubadd n.+1 m 1)).
n, m: nat
l: n.+1 <= m
IHl: n.+1 - m = 0
n.+1 - m - 1 = 0
      destruct (symmetric_paths _ _ IHl).
n, m: nat
l: n.+1 <= m
IHl: 0 = 0
0 - 1 = 0
      reflexivity.
Defined.

Proposition sub_leq_0_converse (n m : nat) : n - m = 0 -> n <= m.
n, m: nat
n - m = 0 -> n <= m
Proof.
n, m: nat
n - m = 0 -> n <= m
  revert m; simple_induction n n IHn.
forall m : nat, 0 - m = 0 -> 0 <= m
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
forall m : nat, n.+1 - m = 0 -> n.+1 <= m
  -
forall m : nat, 0 - m = 0 -> 0 <= m auto with nat.
  -
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
forall m : nat, n.+1 - m = 0 -> n.+1 <= m intros m eq.
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
m: nat
eq: n.+1 - m = 0
n.+1 <= m destruct m.
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
eq: n.+1 - 0 = 0
n.+1 <= 0
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
m: nat
eq: n.+1 - m.+1 = 0
n.+1 <= m.+1
    +
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
eq: n.+1 - 0 = 0
n.+1 <= 0 simpl in eq.
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
eq: n.+1 = 0
n.+1 <= 0 apply symmetric_paths in eq.
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
eq: 0 = n.+1
n.+1 <= 0
      contradiction (not_eq_O_S n eq).
    +
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
m: nat
eq: n.+1 - m.+1 = 0
n.+1 <= m.+1 simpl in eq.
n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
m: nat
eq: n - m = 0
n.+1 <= m.+1 apply leq_S_n', IHn, eq.
Defined.

Proposition sub_gt_0_lt (n m : nat) : n - m > 0 -> m < n.
n, m: nat
n - m > 0 -> m < n
Proof.
n, m: nat
n - m > 0 -> m < n
  intro ineq.
n, m: nat
ineq: n - m > 0
m < n
  destruct (@leq_dichot n m) as [n_leq_m |]; [ | assumption].
n, m: nat
ineq: n - m > 0
n_leq_m: n <= m
m < n
  apply sub_leq_0 in n_leq_m.
n, m: nat
ineq: n - m > 0
n_leq_m: n - m = 0
m < n
  contradiction (not_lt_n_n 0).
n, m: nat
ineq: n - m > 0
n_leq_m: n - m = 0
0 < 0 now rewrite n_leq_m in ineq.
Defined.

Proposition lt_sub_gt_0 (n m : nat) : m < n -> 0 < n - m.
n, m: nat
m < n -> 0 < n - m
Proof.
n, m: nat
m < n -> 0 < n - m
  revert m; simple_induction n n IHn.
forall m : nat, m < 0 -> 0 < 0 - m
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
forall m : nat, m < n.+1 -> 0 < n.+1 - m
  -
forall m : nat, m < 0 -> 0 < 0 - m intros m ineq.
m: nat
ineq: m < 0
0 < 0 - m contradiction (not_lt_n_0 m).
  -
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
forall m : nat, m < n.+1 -> 0 < n.+1 - m destruct m.
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
0 < n.+1 -> 0 < n.+1 - 0
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
m: nat
m.+1 < n.+1 -> 0 < n.+1 - m.+1
    +
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
0 < n.+1 -> 0 < n.+1 - 0 simpl.
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
0 < n.+1 -> 0 < n.+1 easy.
    +
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
m: nat
m.+1 < n.+1 -> 0 < n.+1 - m.+1 simpl.
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
m: nat
m.+1 < n.+1 -> 0 < n - m intro ineq.
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
m: nat
ineq: m.+1 < n.+1
0 < n - m apply leq_S_n in ineq.
n: nat
IHn: forall m : nat, m < n -> 0 < n - m
m: nat
ineq: m.+1 <= n
0 < n - m
      now apply IHn in ineq.
Defined.

Proposition natminuspluseq (n m : nat)
  : n <= m -> (m - n) + n = m.
n, m: nat
n <= m -> m - n + n = m
Proof.
n, m: nat
n <= m -> m - n + n = m
  revert m; simple_induction n n IHn.
forall m : nat, 0 <= m -> m - 0 + 0 = m
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
forall m : nat, n.+1 <= m -> m - n.+1 + n.+1 = m
  -
forall m : nat, 0 <= m -> m - 0 + 0 = m intros.
m: nat
H: 0 <= m
m - 0 + 0 = m destruct m; [reflexivity |].
m: nat
H: 0 <= m.+1
m.+1 - 0 + 0 = m.+1 simpl.
m: nat
H: 0 <= m.+1
(m + 0).+1 = m.+1
    apply (ap S), symmetric_paths, add_n_O.
  -
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
forall m : nat, n.+1 <= m -> m - n.+1 + n.+1 = m intros m l.
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
m: nat
l: n.+1 <= m
m - n.+1 + n.+1 = m destruct m.
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
l: n.+1 <= 0
0 - n.+1 + n.+1 = 0
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
m: nat
l: n.+1 <= m.+1
m.+1 - n.+1 + n.+1 = m.+1
    +
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
l: n.+1 <= 0
0 - n.+1 + n.+1 = 0 contradiction (not_leq_Sn_0 n).
    +
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
m: nat
l: n.+1 <= m.+1
m.+1 - n.+1 + n.+1 = m.+1 simpl.
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
m: nat
l: n.+1 <= m.+1
m - n + n.+1 = m.+1 apply leq_S_n, IHn in l.
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
m: nat
l: m - n + n = m
m - n + n.+1 = m.+1
      destruct (nat_add_n_Sm (m - n) n).
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
m: nat
l: m - n + n = m
(m - n + n).+1 = m.+1
      destruct (symmetric_paths _ _ l).
n: nat
IHn: forall m : nat, n <= m -> m - n + n = m
m: nat
l: m = m
m.+1 = m.+1
      reflexivity.
Defined.

Proposition natminusplusineq (n m : nat) : n <= n - m + m.
n, m: nat
n <= n - m + m
Proof.
n, m: nat
n <= n - m + m
  destruct (@leq_dichot m n) as [l | g].
n, m: nat
l: m <= n
n <= n - m + m
n, m: nat
g: m > n
n <= n - m + m
  -
n, m: nat
l: m <= n
n <= n - m + m destruct (symmetric_paths _ _ (natminuspluseq _ _ l));
      constructor.
  -
n, m: nat
g: m > n
n <= n - m + m apply n_lt_m_n_leq_m in g.
n, m: nat
g: n <= m
n <= n - m + m
    now destruct (symmetric_paths _ _ (sub_leq_0 n m _)).
Defined.

Proposition natminuspluseq' (n m : nat)
  : n <= m -> n + (m - n) = m.
n, m: nat
n <= m -> n + (m - n) = m
Proof.
n, m: nat
n <= m -> n + (m - n) = m
  intros.
n, m: nat
H: n <= m
n + (m - n) = m destruct (symmetric_paths _ _ (nat_add_comm n (m - n))).
n, m: nat
H: n <= m
m - n + n = m
  apply natminuspluseq.
n, m: nat
H: n <= m
n <= m assumption.
Defined.

#[export] Hint Rewrite -> natminuspluseq : nat.
#[export] Hint Rewrite -> natminuspluseq' : nat.

Lemma equiv_leq_add n m
  : leq n m <~> exists k, k + n = m.
n, m: nat
n <= m <~> {k : nat & k + n = m}
Proof.
n, m: nat
n <= m <~> {k : nat & k + n = m}
  srapply equiv_iff_hprop.
n, m: nat
IsHProp {k : nat & k + n = m}
n, m: nat
n <= m -> {k : nat & k + n = m}
n, m: nat
{k : nat & k + n = m} -> n <= m
  -
n, m: nat
IsHProp {k : nat & k + n = m} apply hprop_allpath.
n, m: nat
forall x y : {k : nat & k + n = m}, x = y
    intros [x p] [y q].
n, m, x: nat
p: x + n = m
y: nat
q: y + n = m
(x; p) = (y; q)
    pose (r := summand_is_sub x _ _ p @ (summand_is_sub y _ _ q)^).
n, m, x: nat
p: x + n = m
y: nat
q: y + n = m
r:= summand_is_sub x m n p @ (summand_is_sub y m n q)^: x = y
(x; p) = (y; q)
    destruct r.
n, m, x: nat
p, q: x + n = m
(x; p) = (x; q)
    apply ap.
n, m, x: nat
p, q: x + n = m
p = q
    apply path_ishprop.
  -
n, m: nat
n <= m -> {k : nat & k + n = m} intros p.
n, m: nat
p: n <= m
{k : nat & k + n = m}
    exists (m - n).
n, m: nat
p: n <= m
m - n + n = m
    apply natminuspluseq, p.
  -
n, m: nat
{k : nat & k + n = m} -> n <= m intros [k p].
n, m, k: nat
p: k + n = m
n <= m
    destruct p.
n, k: nat
n <= k + n
    apply leq_add.
Defined.

#[export] Hint Resolve leq_S_n' : nat.

Ltac leq_S_n_in_hypotheses :=
  match goal with
  | [ H : ?n.+1 <= ?m.+1 |- _ ] => apply leq_S_n in H
  | [ H : ?n < ?m.+1 |- _ ] => apply leq_S_n in H
  | [ H : ?m.+1 > ?n |- _ ] => apply leq_S_n in H
  | [ H : ?m.+1 >= ?n.+1 |- _ ] => apply leq_S_n in H
  end.

#[export] Hint Extern 4 => leq_S_n_in_hypotheses : nat.

Proposition nataddpreservesleq { n m k : nat }
  : n <= m -> n + k <= m + k.
n, m, k: nat
n <= m -> n + k <= m + k
Proof.
n, m, k: nat
n <= m -> n + k <= m + k
  intro l.
n, m, k: nat
l: n <= m
n + k <= m + k
  simple_induction k k IHk.
n, m: nat
l: n <= m
n + 0 <= m + 0
n, m: nat
l: n <= m
k: nat
IHk: n + k <= m + k
n + k.+1 <= m + k.+1
  -
n, m: nat
l: n <= m
n + 0 <= m + 0 destruct (add_n_O n), (add_n_O m); exact l.
  -
n, m: nat
l: n <= m
k: nat
IHk: n + k <= m + k
n + k.+1 <= m + k.+1 destruct (nat_add_n_Sm n k), (nat_add_n_Sm m k);
      apply leq_S_n'; exact IHk.
Defined.

#[export] Hint Resolve nataddpreservesleq : nat.

Proposition nataddpreservesleq' { n m k : nat }
  : n <= m -> k + n <= k + m.
n, m, k: nat
n <= m -> k + n <= k + m
Proof.
n, m, k: nat
n <= m -> k + n <= k + m
  destruct (symmetric_paths _ _ (nat_add_comm k m)),
    (symmetric_paths _ _ (nat_add_comm k n)).
n, m, k: nat
n <= m -> n + k <= m + k
  exact nataddpreservesleq.
Defined.

#[export] Hint Resolve nataddpreservesleq' : nat.

Proposition nataddpreserveslt { n m k : nat }
  : n < m -> n + k < m + k.
n, m, k: nat
n < m -> n + k < m + k
Proof.
n, m, k: nat
n < m -> n + k < m + k
  unfold "<".
n, m, k: nat
n.+1 <= m -> (n + k).+1 <= m + k
  change (n + k).+1 with (n.+1 + k).
n, m, k: nat
n.+1 <= m -> n.+1 + k <= m + k
  generalize (n.+1).
n, m, k: nat
forall n : nat, n <= m -> n + k <= m + k intros n' l.
n, m, k, n': nat
l: n' <= m
n' + k <= m + k
  simple_induction k k IHk.
n, m, n': nat
l: n' <= m
n' + 0 <= m + 0
n, m, n': nat
l: n' <= m
k: nat
IHk: n' + k <= m + k
n' + k.+1 <= m + k.+1
  -
n, m, n': nat
l: n' <= m
n' + 0 <= m + 0 destruct (add_n_O n'), (add_n_O m); exact l.
  -
n, m, n': nat
l: n' <= m
k: nat
IHk: n' + k <= m + k
n' + k.+1 <= m + k.+1 destruct (nat_add_n_Sm n' k), (nat_add_n_Sm m k);
      apply leq_S_n'; exact IHk.
Defined.

Proposition nataddpreserveslt' { n m k : nat }
  : n < m -> k + n < k + m.
n, m, k: nat
n < m -> k + n < k + m
Proof.
n, m, k: nat
n < m -> k + n < k + m
  destruct (symmetric_paths _ _ (nat_add_comm k n)),
    (symmetric_paths _ _ (nat_add_comm k m));
    exact nataddpreserveslt.
Defined.

Proposition nataddreflectslt { n m k : nat }
  : n + k < m + k -> n < m.
n, m, k: nat
n + k < m + k -> n < m
Proof.
n, m, k: nat
n + k < m + k -> n < m
  simple_induction k k IHk.
n, m: nat
n + 0 < m + 0 -> n < m
n, m, k: nat
IHk: n + k < m + k -> n < m
n + k.+1 < m + k.+1 -> n < m
  -
n, m: nat
n + 0 < m + 0 -> n < m destruct (add_n_O n), (add_n_O m); trivial.
  -
n, m, k: nat
IHk: n + k < m + k -> n < m
n + k.+1 < m + k.+1 -> n < m intro l.
n, m, k: nat
IHk: n + k < m + k -> n < m
l: n + k.+1 < m + k.+1
n < m destruct (nat_add_n_Sm n k), (nat_add_n_Sm m k) in l.
n, m, k: nat
IHk: n + k < m + k -> n < m
l: (n + k).+1 < (m + k).+1
n < m
    apply leq_S_n, IHk in l; exact l.
Defined.

Proposition nataddreflectsleq { n m k : nat }
  : n + k <= m + k -> n <= m.
n, m, k: nat
n + k <= m + k -> n <= m
Proof.
n, m, k: nat
n + k <= m + k -> n <= m
  destruct n.
m, k: nat
0 + k <= m + k -> 0 <= m
n, m, k: nat
n.+1 + k <= m + k -> n.+1 <= m
  -
m, k: nat
0 + k <= m + k -> 0 <= m intros ?; apply leq_0_n.
  -
n, m, k: nat
n.+1 + k <= m + k -> n.+1 <= m intro a.
n, m, k: nat
a: n.+1 + k <= m + k
n.+1 <= m change (n.+1 + k) with (n + k).+1 in a.
n, m, k: nat
a: (n + k).+1 <= m + k
n.+1 <= m
    now apply (@nataddreflectslt n m k).
Defined.

Proposition nataddreflectslt' { n m k : nat }
  : k + n < k + m -> n < m.
n, m, k: nat
k + n < k + m -> n < m
Proof.
n, m, k: nat
k + n < k + m -> n < m
  destruct (symmetric_paths _ _ (nat_add_comm k n)),
    (symmetric_paths _ _ (nat_add_comm k m));
    exact nataddreflectslt.
Defined.

Proposition nataddreflectsleq' { n m k : nat }
  : k + n <= k + m -> n <= m.
n, m, k: nat
k + n <= k + m -> n <= m
Proof.
n, m, k: nat
k + n <= k + m -> n <= m
  destruct (symmetric_paths _ _ (nat_add_comm k n)),
    (symmetric_paths _ _ (nat_add_comm k m));
    exact nataddreflectsleq.
Defined.

Proposition natsubreflectsleq { n m k : nat }
  : k <= m -> n - k <= m - k -> n <= m.
n, m, k: nat
k <= m -> n - k <= m - k -> n <= m
Proof.
n, m, k: nat
k <= m -> n - k <= m - k -> n <= m
  intros ineq1 ineq2.
n, m, k: nat
ineq1: k <= m
ineq2: n - k <= m - k
n <= m
  apply (@nataddpreservesleq _ _ k) in ineq2.
n, m, k: nat
ineq1: k <= m
ineq2: n - k + k <= m - k + k
n <= m
  apply (@leq_trans _ (n - k + k) _ (natminusplusineq _ _)).
n, m, k: nat
ineq1: k <= m
ineq2: n - k + k <= m - k + k
n - k + k <= m
  apply (@leq_trans _ (m - k + k)  _ _).
n, m, k: nat
ineq1: k <= m
ineq2: n - k + k <= m - k + k
m - k + k <= m
  destruct (symmetric_paths _ _ (natminuspluseq k m ineq1)); easy.
Defined.

Proposition nataddsub_assoc_lemma {k m : nat}
  : (k <= m) -> m.+1 - k = (m - k).+1.
k, m: nat
k <= m -> m.+1 - k = (m - k).+1
Proof.
k, m: nat
k <= m -> m.+1 - k = (m - k).+1
  revert m; simple_induction k k IHk.
forall m : nat, 0 <= m -> m.+1 - 0 = (m - 0).+1
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
forall m : nat,
k.+1 <= m -> m.+1 - k.+1 = (m - k.+1).+1
  -
forall m : nat, 0 <= m -> m.+1 - 0 = (m - 0).+1 intros m l; simpl.
m: nat
l: 0 <= m
m.+1 = (m - 0).+1 destruct m; reflexivity.
  -
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
forall m : nat,
k.+1 <= m -> m.+1 - k.+1 = (m - k.+1).+1 destruct m.
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
k.+1 <= 0 -> 1 - k.+1 = (0 - k.+1).+1
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
m: nat
k.+1 <= m.+1 -> m.+2 - k.+1 = (m.+1 - k.+1).+1
    +
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
k.+1 <= 0 -> 1 - k.+1 = (0 - k.+1).+1 simpl; intro g; contradiction (not_leq_Sn_0 _ g).
    +
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
m: nat
k.+1 <= m.+1 -> m.+2 - k.+1 = (m.+1 - k.+1).+1 intro l; apply leq_S_n in l.
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
m: nat
l: k <= m
m.+2 - k.+1 = (m.+1 - k.+1).+1
      change (m.+2 - k.+1) with (m.+1 - k).
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
m: nat
l: k <= m
m.+1 - k = (m.+1 - k.+1).+1
      change (m.+1 - k.+1) with (m - k).
k: nat
IHk: forall m : nat, k <= m -> m.+1 - k = (m - k).+1
m: nat
l: k <= m
m.+1 - k = (m - k).+1
      exact (IHk _ l).
Defined.

Proposition nataddsub_assoc (n : nat) {m k : nat}
  : (k <= m) -> n + (m - k) = n + m - k.
n, m, k: nat
k <= m -> n + (m - k) = n + m - k
Proof.
n, m, k: nat
k <= m -> n + (m - k) = n + m - k
  revert m k.
n: nat
forall m k : nat, k <= m -> n + (m - k) = n + m - k simple_induction n n IHn.
forall m k : nat, k <= m -> 0 + (m - k) = 0 + m - k
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
forall m k : nat,
k <= m -> n.+1 + (m - k) = n.+1 + m - k
  -
forall m k : nat, k <= m -> 0 + (m - k) = 0 + m - k reflexivity.
  -
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
forall m k : nat,
k <= m -> n.+1 + (m - k) = n.+1 + m - k intros m k l.
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k <= m
n.+1 + (m - k) = n.+1 + m - k
    change (n.+1 + (m - k)) with (n + (m - k)).+1;
      change (n.+1 + m) with (n +m).+1.
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k <= m
(n + (m - k)).+1 = (n + m).+1 - k
    destruct k, m;
      [ reflexivity
      | reflexivity
      | contradiction (not_lt_n_0 k _)
      | ].
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k.+1 <= m.+1
(n + (m.+1 - k.+1)).+1 = (n + m.+1).+1 - k.+1
    simpl "-".
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k.+1 <= m.+1
(n + (m - k)).+1 = n + m.+1 - k apply leq_S_n in l.
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k <= m
(n + (m - k)).+1 = n + m.+1 - k
    destruct (symmetric_paths _ _ (nat_add_n_Sm n (m - k))).
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k <= m
n + (m - k).+1 = n + m.+1 - k
    destruct  (nataddsub_assoc_lemma l).
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k <= m
n + (m.+1 - k) = n + m.+1 - k
    apply (IHn m.+1 k).
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k <= m
k <= m.+1
    apply leq_S.
n: nat
IHn: forall m k : nat, k <= m -> n + (m - k) = n + m - k
m, k: nat
l: k <= m
k <= m
    assumption.
Defined.

Proposition nataddsub_comm (n m k : nat)
  : m <= n -> (n - m) + k = (n + k) - m.
n, m, k: nat
m <= n -> n - m + k = n + k - m
Proof.
n, m, k: nat
m <= n -> n - m + k = n + k - m
  intro l.
n, m, k: nat
l: m <= n
n - m + k = n + k - m
  destruct (nat_add_comm k n).
n, m, k: nat
l: m <= n
n - m + k = k + n - m
  destruct (nataddsub_assoc k l).
n, m, k: nat
l: m <= n
n - m + k = k + (n - m)
  apply nat_add_comm.
Defined.

Proposition nataddsub_comm_ineq_lemma (n m : nat)
  : n.+1 - m <= (n - m).+1.
n, m: nat
n.+1 - m <= (n - m).+1
Proof.
n, m: nat
n.+1 - m <= (n - m).+1
  revert m.
n: nat
forall m : nat, n.+1 - m <= (n - m).+1
  simple_induction n n IHn.
forall m : nat, 1 - m <= (0 - m).+1
n: nat
IHn: forall m : nat, n.+1 - m <= (n - m).+1
forall m : nat, n.+2 - m <= (n.+1 - m).+1
  -
forall m : nat, 1 - m <= (0 - m).+1 simple_induction m m IHm; [ apply leq_n | apply leq_S; apply leq_n ]. 
  -
n: nat
IHn: forall m : nat, n.+1 - m <= (n - m).+1
forall m : nat, n.+2 - m <= (n.+1 - m).+1 intro m; simple_induction m m IHm.
n: nat
IHn: forall m : nat, n.+1 - m <= (n - m).+1
n.+2 - 0 <= (n.+1 - 0).+1
n: nat
IHn: forall m : nat, n.+1 - m <= (n - m).+1
m: nat
IHm: n.+2 - m <= (n.+1 - m).+1
n.+2 - m.+1 <= (n.+1 - m.+1).+1
    +
n: nat
IHn: forall m : nat, n.+1 - m <= (n - m).+1
n.+2 - 0 <= (n.+1 - 0).+1 apply leq_n.
    +
n: nat
IHn: forall m : nat, n.+1 - m <= (n - m).+1
m: nat
IHm: n.+2 - m <= (n.+1 - m).+1
n.+2 - m.+1 <= (n.+1 - m.+1).+1 apply IHn.
Defined.

Proposition nataddsub_comm_ineq (n m k : nat)
  : (n + k) - m <= (n - m) + k.
n, m, k: nat
n + k - m <= n - m + k
Proof.
n, m, k: nat
n + k - m <= n - m + k 
  simple_induction k k IHk.
n, m: nat
n + 0 - m <= n - m + 0
n, m, k: nat
IHk: n + k - m <= n - m + k
n + k.+1 - m <= n - m + k.+1
  -
n, m: nat
n + 0 - m <= n - m + 0 destruct (add_n_O n), (add_n_O (n - m)); constructor.
  -
n, m, k: nat
IHk: n + k - m <= n - m + k
n + k.+1 - m <= n - m + k.+1 destruct (add_n_Sm n k).
n, m, k: nat
IHk: n + k - m <= n - m + k
(n + k).+1 - m <= n - m + k.+1
    refine (leq_trans (nataddsub_comm_ineq_lemma (n+k) m) _).
n, m, k: nat
IHk: n + k - m <= n - m + k
(n + k - m).+1 <= n - m + k.+1
    destruct (add_n_Sm (n - m) k).
n, m, k: nat
IHk: n + k - m <= n - m + k
(n + k - m).+1 <= (n - m + k).+1
    now apply leq_S_n'.
Defined.

Proposition nat_sub_add_ineq (n m : nat) : n <= n - m + m.
n, m: nat
n <= n - m + m
Proof.
n, m: nat
n <= n - m + m
  destruct (@leq_dichot m n) as [l | gt].
n, m: nat
l: m <= n
n <= n - m + m
n, m: nat
gt: m > n
n <= n - m + m
  -
n, m: nat
l: m <= n
n <= n - m + m destruct (symmetric_paths _ _ (nataddsub_comm _ _ m l)).
n, m: nat
l: m <= n
n <= n + m - m
    destruct (symmetric_paths _ _ (add_n_sub_n_eq n m)).
n, m: nat
l: m <= n
n <= n
    apply leq_refl; done.
  -
n, m: nat
gt: m > n
n <= n - m + m apply n_lt_m_n_leq_m in gt.
n, m: nat
gt: n <= m
n <= n - m + m
    destruct (symmetric_paths _ _ (sub_leq_0 n m _)).
n, m: nat
gt: n <= m
n <= 0 + m
    assumption.
Defined.

Proposition i_lt_n_sum_m (n m i : nat)
  : i < n - m -> m <= n.
n, m, i: nat
i < n - m -> m <= n
Proof.
n, m, i: nat
i < n - m -> m <= n
  revert m i; simple_induction n n IHn.
forall m i : nat, i < 0 - m -> m <= 0
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
forall m i : nat, i < n.+1 - m -> m <= n.+1
  -
forall m i : nat, i < 0 - m -> m <= 0 intros m i l.
m, i: nat
l: i < 0 - m
m <= 0 simpl in l.
m, i: nat
l: i < 0
m <= 0 contradiction (not_lt_n_0 _ _).
  -
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
forall m i : nat, i < n.+1 - m -> m <= n.+1 intros m i l.
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
m, i: nat
l: i < n.+1 - m
m <= n.+1 destruct m.
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
i: nat
l: i < n.+1 - 0
0 <= n.+1
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
m, i: nat
l: i < n.+1 - m.+1
m.+1 <= n.+1
    +
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
i: nat
l: i < n.+1 - 0
0 <= n.+1 apply leq_0_n.
    +
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
m, i: nat
l: i < n.+1 - m.+1
m.+1 <= n.+1 apply leq_S_n'.
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
m, i: nat
l: i < n.+1 - m.+1
m <= n simpl in l.
n: nat
IHn: forall m i : nat, i < n - m -> m <= n
m, i: nat
l: i < n - m
m <= n apply (IHn m i l).
Defined.

Proposition nataddsub_assoc_implication (n : nat) {m k z : nat}
  : (k <= m) -> n + (m - k) = z -> n + m - k = z.
n, m, k, z: nat
k <= m -> n + (m - k) = z -> n + m - k = z
Proof.
n, m, k, z: nat
k <= m -> n + (m - k) = z -> n + m - k = z
  intro H.
n, m, k, z: nat
H: k <= m
n + (m - k) = z -> n + m - k = z
  destruct (symmetric_paths _ _ (nataddsub_assoc n H)); done.
Defined.

#[export] Hint Resolve nataddsub_assoc_implication : nat.

Proposition nat_add_sub_eq (n : nat) {k: nat}
  : (k <= n) -> k + (n - k) = n.
n, k: nat
k <= n -> k + (n - k) = n
Proof.
n, k: nat
k <= n -> k + (n - k) = n
  intro H.
n, k: nat
H: k <= n
k + (n - k) = n
  destruct (symmetric_paths _ _ (nataddsub_assoc k H));
  destruct (nat_add_comm n k); exact (add_n_sub_n_eq _ _).
Defined.

#[export] Hint Resolve nat_add_sub_eq : nat.

Proposition predeqminus1 { n : nat } : n - 1 = pred n.
n: nat
n - 1 = pred n
Proof.
n: nat
n - 1 = pred n
  simple_induction' n.
0 - 1 = pred 0
n: nat
IH: n - 1 = pred n
n.+1 - 1 = pred n.+1
  -
0 - 1 = pred 0 reflexivity.
  -
n: nat
IH: n - 1 = pred n
n.+1 - 1 = pred n.+1 apply sub_n_0.
Defined.

Proposition predn_leq_n (n : nat) : pred n <= n.
n: nat
pred n <= n
Proof.
n: nat
pred n <= n
  case n; [ apply leq_n | intro; apply leq_S; apply leq_n].
Defined.

#[export] Hint Resolve predn_leq_n : nat.

Proposition S_predn (n i: nat) : (i < n) -> S(pred n) = n.
n, i: nat
i < n -> (pred n).+1 = n
Proof.
n, i: nat
i < n -> (pred n).+1 = n
  simple_induction' n; intros l.
i: nat
l: i < 0
(pred 0).+1 = 0
i, n: nat
IH: i < n -> (pred n).+1 = n
l: i < n.+1
(pred n.+1).+1 = n.+1
  -
i: nat
l: i < 0
(pred 0).+1 = 0 contradiction (not_lt_n_0 i).
  -
i, n: nat
IH: i < n -> (pred n).+1 = n
l: i < n.+1
(pred n.+1).+1 = n.+1 reflexivity.
Defined.

#[export] Hint Rewrite S_predn : nat.
#[export] Hint Rewrite <- pred_Sn : nat.

#[export] Hint Resolve S_predn : nat.
#[export] Hint Resolve leq_n_pred : nat.

Proposition pred_equiv (k n : nat) : k < n -> k < S (pred n).
k, n: nat
k < n -> k < (pred n).+1
Proof.
k, n: nat
k < n -> k < (pred n).+1 
  intro ineq; destruct n.
k: nat
ineq: k < 0
k < (pred 0).+1
k, n: nat
ineq: k < n.+1
k < (pred n.+1).+1
  -
k: nat
ineq: k < 0
k < (pred 0).+1 contradiction (not_lt_n_0 _ _).
  -
k, n: nat
ineq: k < n.+1
k < (pred n.+1).+1 assumption.
Defined.

Proposition n_leq_pred_Sn (n : nat) : n <= S (pred n).
n: nat
n <= (pred n).+1
Proof.
n: nat
n <= (pred n).+1 
  destruct n; auto.
Defined.

Proposition leq_implies_pred_lt (i n k : nat)
  : (n > i) -> n <= k -> pred n < k.
i, n, k: nat
n > i -> n <= k -> pred n < k
Proof.
i, n, k: nat
n > i -> n <= k -> pred n < k
  intro ineq; destruct n.
i, k: nat
ineq: 0 > i
0 <= k -> pred 0 < k
i, n, k: nat
ineq: n.+1 > i
n.+1 <= k -> pred n.+1 < k
  -
i, k: nat
ineq: 0 > i
0 <= k -> pred 0 < k contradiction (not_lt_n_0 i).
  -
i, n, k: nat
ineq: n.+1 > i
n.+1 <= k -> pred n.+1 < k intro; assumption.
Defined.

Proposition pred_lt_implies_leq (n k : nat)
  : pred n < k -> n <= k.
n, k: nat
pred n < k -> n <= k
Proof.
n, k: nat
pred n < k -> n <= k
  intro l; destruct n.
k: nat
l: pred 0 < k
0 <= k
n, k: nat
l: pred n.+1 < k
n.+1 <= k
  -
k: nat
l: pred 0 < k
0 <= k apply leq_0_n.
  -
n, k: nat
l: pred n.+1 < k
n.+1 <= k assumption.
Defined.

Proposition lt_implies_pred_geq (i j : nat) : i < j -> i <= pred j.
i, j: nat
i < j -> i <= pred j
Proof.
i, j: nat
i < j -> i <= pred j
  intro l; apply leq_n_pred in l; assumption.
Defined.

#[export] Hint Resolve lt_implies_pred_geq : nat.

Proposition j_geq_0_lt_implies_pred_geq (i j k : nat)
  : i < j -> k.+1 <= j -> k <= pred j.
i, j, k: nat
i < j -> k.+1 <= j -> k <= pred j
Proof.
i, j, k: nat
i < j -> k.+1 <= j -> k <= pred j
  intros l ineq.
i, j, k: nat
l: i < j
ineq: k.+1 <= j
k <= pred j
  destruct j.
i, k: nat
l: i < 0
ineq: k.+1 <= 0
k <= pred 0
i, j, k: nat
l: i < j.+1
ineq: k.+1 <= j.+1
k <= pred j.+1
  -
i, k: nat
l: i < 0
ineq: k.+1 <= 0
k <= pred 0 contradiction (not_lt_n_0 i).
  -
i, j, k: nat
l: i < j.+1
ineq: k.+1 <= j.+1
k <= pred j.+1 now simpl; apply leq_S_n.
Defined.

#[export] Hint Resolve lt_implies_pred_geq : nat.

Proposition pred_gt_implies_lt (i j : nat)
  : i < pred j -> i.+1 < j.
i, j: nat
i < pred j -> i.+1 < j
Proof.
i, j: nat
i < pred j -> i.+1 < j
  intros ineq.
i, j: nat
ineq: i < pred j
i.+1 < j
  assert (H := leq_S_n' _ _ ineq).
i, j: nat
ineq: i < pred j
H: i.+2 <= (pred j).+1
i.+1 < j assert (i < j) as X.
i, j: nat
ineq: i < pred j
H: i.+2 <= (pred j).+1
i < j
i, j: nat
ineq: i < pred j
H: i.+2 <= (pred j).+1
X: i < j
i.+1 < j {
i, j: nat
ineq: i < pred j
H: i.+2 <= (pred j).+1
i < j
    apply (@mixed_trans2 _ (pred j) _);
      [assumption  | apply predn_leq_n].
  }
i, j: nat
ineq: i < pred j
H: i.+2 <= (pred j).+1
X: i < j
i.+1 < j
  destruct (symmetric_paths _ _ (S_predn _ _ X)) in H.
i, j: nat
ineq: i < pred j
H: i.+2 <= j
X: i < j
i.+1 < j
  assumption.
Defined.

Proposition pred_preserves_lt {i n: nat} (p : i < n) m
  : (n < m) -> (pred n < pred m).
i, n: nat
p: i < n
m: nat
n < m -> pred n < pred m
Proof.
i, n: nat
p: i < n
m: nat
n < m -> pred n < pred m
  intro l.
i, n: nat
p: i < n
m: nat
l: n < m
pred n < pred m
  apply leq_S_n.
i, n: nat
p: i < n
m: nat
l: n < m
(pred n).+2 <= (pred m).+1 destruct (symmetric_paths _ _ (S_predn n i _)).
i, n: nat
p: i < n
m: nat
l: n < m
n.+1 <= (pred m).+1
  set (k :=  transitive_lt i n m p l).
i, n: nat
p: i < n
m: nat
l: n < m
k:= transitive_lt i n m p l: i < m
n.+1 <= (pred m).+1
  destruct (symmetric_paths _ _ (S_predn m i _)).
i, n: nat
p: i < n
m: nat
l: n < m
k:= transitive_lt i n m p l: i < m
n.+1 <= m
  assumption.
Defined.

Proposition natsubpreservesleq { n m k : nat }
  : n <= m -> n - k <= m - k.
n, m, k: nat
n <= m -> n - k <= m - k
Proof.
n, m, k: nat
n <= m -> n - k <= m - k
  simple_induction k k IHk.
n, m: nat
n <= m -> n - 0 <= m - 0
n, m, k: nat
IHk: n <= m -> n - k <= m - k
n <= m -> n - k.+1 <= m - k.+1
  -
n, m: nat
n <= m -> n - 0 <= m - 0 destruct (symmetric_paths _ _ (sub_n_0 n)),
      (symmetric_paths _ _ (sub_n_0 m)); done.
  -
n, m, k: nat
IHk: n <= m -> n - k <= m - k
n <= m -> n - k.+1 <= m - k.+1 intro l.
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
n - k.+1 <= m - k.+1 change (k.+1) with (1 + k).
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
n - (1 + k) <= m - (1 + k)
    destruct (nat_add_comm k 1).
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
n - (k + 1) <= m - (k + 1)
    destruct (symmetric_paths _ _ (subsubadd n k 1)).
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
n - k - 1 <= m - (k + 1)
    destruct (symmetric_paths _ _ (subsubadd m k 1)).
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
n - k - 1 <= m - k - 1
    destruct (symmetric_paths _ _ (@predeqminus1 (n -k))).
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
pred (n - k) <= m - k - 1
    destruct (symmetric_paths _ _ (@predeqminus1 (m -k))).
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
pred (n - k) <= pred (m - k)
    apply leq_n_pred, IHk.
n, m, k: nat
IHk: n <= m -> n - k <= m - k
l: n <= m
n <= m exact l.
Defined.

#[export] Hint Resolve natsubpreservesleq : nat.

Proposition sub_less { n k : nat } : n - k <= n.
n, k: nat
n - k <= n
Proof.
n, k: nat
n - k <= n
  revert k.
n: nat
forall k : nat, n - k <= n
  simple_induction n n IHn.
forall k : nat, 0 - k <= 0
n: nat
IHn: forall k : nat, n - k <= n
forall k : nat, n.+1 - k <= n.+1
  -
forall k : nat, 0 - k <= 0 intros; apply leq_0_n.
  -
n: nat
IHn: forall k : nat, n - k <= n
forall k : nat, n.+1 - k <= n.+1 destruct k.
n: nat
IHn: forall k : nat, n - k <= n
n.+1 - 0 <= n.+1
n: nat
IHn: forall k : nat, n - k <= n
k: nat
n.+1 - k.+1 <= n.+1
    +
n: nat
IHn: forall k : nat, n - k <= n
n.+1 - 0 <= n.+1 apply leq_n.
    +
n: nat
IHn: forall k : nat, n - k <= n
k: nat
n.+1 - k.+1 <= n.+1 simpl; apply (@leq_trans _ n _);
        [ apply IHn | apply leq_S, leq_n].
Defined.

#[export] Hint Resolve sub_less : nat.
#[export] Hint Resolve leq_S_n' : nat.

Proposition sub_less_strict { n k : nat }
  : 0 < n -> 0 < k -> n - k < n.
n, k: nat
0 < n -> 0 < k -> n - k < n
Proof.
n, k: nat
0 < n -> 0 < k -> n - k < n
  intros l l'.
n, k: nat
l: 0 < n
l': 0 < k
n - k < n
  unfold "<".
n, k: nat
l: 0 < n
l': 0 < k
(n - k).+1 <= n
  destruct k, n;
  try (contradiction (not_lt_n_0 _ _)).
n, k: nat
l: 0 < n.+1
l': 0 < k.+1
(n.+1 - k.+1).+1 <= n.+1
  simpl; apply leq_S_n', sub_less.
Defined.

Proposition natpmswap1 (k m n : nat)
  : n <= k -> k < n + m -> k - n < m.
k, m, n: nat
n <= k -> k < n + m -> k - n < m
Proof.
k, m, n: nat
n <= k -> k < n + m -> k - n < m
  intros l q.
k, m, n: nat
l: n <= k
q: k < n + m
k - n < m
  assert (q' : k - n + n < m + n) by
    (destruct (symmetric_paths _ _ (natminuspluseq n k l));
     destruct (nat_add_comm n m);
     assumption).
k, m, n: nat
l: n <= k
q: k < n + m
q': k - n + n < m + n
k - n < m
  exact (nataddreflectslt q').
Defined.

#[export] Hint Resolve natpmswap1 : nat.

Proposition natpmswap2 (k m n : nat)
  : n <= k -> k - n <= m -> k <= n + m.
k, m, n: nat
n <= k -> k - n <= m -> k <= n + m
Proof.
k, m, n: nat
n <= k -> k - n <= m -> k <= n + m
  intros l q.
k, m, n: nat
l: n <= k
q: k - n <= m
k <= n + m
  apply (@nataddpreservesleq' (k - n) m n) in q.
k, m, n: nat
l: n <= k
q: n + (k - n) <= n + m
k <= n + m
  destruct (symmetric_paths _ _ (nataddsub_assoc n l)) in q.
k, m, n: nat
l: n <= k
q: n + k - n <= n + m
k <= n + m
  destruct (symmetric_paths _ _ (add_n_sub_n_eq' k n)) in q;
    assumption.
Defined.

#[export] Hint Resolve natpmswap2 : nat.

Proposition natpmswap3 (k m n : nat)
  : k <= n -> m <= n - k -> k + m <= n.
k, m, n: nat
k <= n -> m <= n - k -> k + m <= n
Proof.
k, m, n: nat
k <= n -> m <= n - k -> k + m <= n
  intros ineq qe.
k, m, n: nat
ineq: k <= n
qe: m <= n - k
k + m <= n
  apply (@nataddpreservesleq' m (n - k) k) in qe.
k, m, n: nat
ineq: k <= n
qe: k + m <= k + (n - k)
k + m <= n
  destruct (symmetric_paths _ _ (nataddsub_assoc k ineq)) in qe.
k, m, n: nat
ineq: k <= n
qe: k + m <= k + n - k
k + m <= n
  destruct (symmetric_paths _ _ (add_n_sub_n_eq' n k)) in qe;
    assumption.
Defined.

#[export] Hint Resolve natpmswap3 : nat.

Proposition natpmswap4 (k m n : nat)
  : k - n < m -> k < n + m.
k, m, n: nat
k - n < m -> k < n + m
Proof.
k, m, n: nat
k - n < m -> k < n + m
  intro l; apply (@nataddpreserveslt (k - n) m n) in l.
k, m, n: nat
l: k - n + n < m + n
k < n + m
  destruct (nat_add_comm m n).
k, m, n: nat
l: k - n + n < m + n
k < m + n
  now apply (mixed_trans1 k (k - n + n) (m + n)
               (nat_sub_add_ineq _ _)).
Defined.

#[export] Hint Resolve natpmswap4 : nat.

Proposition n_leq_m_n_leq_plus_m_k (n m k : nat)
  : n <= m -> n <= m + k.
n, m, k: nat
n <= m -> n <= m + k
Proof.
n, m, k: nat
n <= m -> n <= m + k
  intro l; apply (leq_trans l); exact (n_leq_add_n_k m k).
Defined.

Proposition nat_add_bifunctor (n n' m m' : nat)
  : n <= m -> n' <= m' -> n + n' <= m + m'.
n, n', m, m': nat
n <= m -> n' <= m' -> n + n' <= m + m'
Proof.
n, n', m, m': nat
n <= m -> n' <= m' -> n + n' <= m + m'
  revert n' m m'; simple_induction n n IHn.
forall n' m m' : nat,
0 <= m -> n' <= m' -> 0 + n' <= m + m'
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
forall n' m m' : nat,
n.+1 <= m -> n' <= m' -> n.+1 + n' <= m + m'
  -
forall n' m m' : nat,
0 <= m -> n' <= m' -> 0 + n' <= m + m' intros n' m m' l l'.
n', m, m': nat
l: 0 <= m
l': n' <= m'
0 + n' <= m + m' simpl.
n', m, m': nat
l: 0 <= m
l': n' <= m'
n' <= m + m'
    apply (leq_trans l').
n', m, m': nat
l: 0 <= m
l': n' <= m'
m' <= m + m' exact (n_leq_add_n_k' m' m).
  -
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
forall n' m m' : nat,
n.+1 <= m -> n' <= m' -> n.+1 + n' <= m + m' intros n' m; destruct m.
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n': nat
forall m' : nat,
n.+1 <= 0 -> n' <= m' -> n.+1 + n' <= 0 + m'
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m: nat
forall m' : nat,
n.+1 <= m.+1 -> n' <= m' -> n.+1 + n' <= m.+1 + m'
    +
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n': nat
forall m' : nat,
n.+1 <= 0 -> n' <= m' -> n.+1 + n' <= 0 + m' intros.
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m': nat
H: n.+1 <= 0
H0: n' <= m'
n.+1 + n' <= 0 + m' contradiction (not_leq_Sn_0 n).
    +
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m: nat
forall m' : nat,
n.+1 <= m.+1 -> n' <= m' -> n.+1 + n' <= m.+1 + m' intros m' l l'.
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m, m': nat
l: n.+1 <= m.+1
l': n' <= m'
n.+1 + n' <= m.+1 + m' apply leq_S_n in l.
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m, m': nat
l: n <= m
l': n' <= m'
n.+1 + n' <= m.+1 + m' simpl.
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m, m': nat
l: n <= m
l': n' <= m'
(n + n').+1 <= (m + m').+1
      apply leq_S_n', IHn.
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m, m': nat
l: n <= m
l': n' <= m'
n <= m
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m, m': nat
l: n <= m
l': n' <= m'
n' <= m'
      *
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m, m': nat
l: n <= m
l': n' <= m'
n <= m exact l.
      *
n: nat
IHn: forall n' m m' : nat, n <= m -> n' <= m' -> n + n' <= m + m'
n', m, m': nat
l: n <= m
l': n' <= m'
n' <= m' exact l'.
Defined.

#[export] Hint Resolve nat_add_bifunctor : nat.
#[export] Hint Resolve nataddpreserveslt : nat.
#[export] Hint Resolve nataddpreservesleq' : nat.
#[export] Hint Resolve nataddpreserveslt' : nat.
#[export] Hint Resolve natineq0eq0 : nat.
#[export] Hint Resolve n_leq_add_n_k : nat.
#[export] Hint Resolve n_leq_m_n_leq_plus_m_k : nat.

#[export] Hint Immediate add_n_sub_n_eq : nat.
#[export] Hint Immediate add_n_sub_n_eq' : nat.

#[export] Hint Rewrite <- add_n_O : nat.
#[export] Hint Rewrite -> add_O_n : nat.
#[export] Hint Rewrite -> add_n_sub_n_eq : nat.
#[export] Hint Rewrite -> add_n_sub_n_eq' : nat.
#[export] Hint Rewrite -> nataddsub_assoc : nat.

Ltac autorewrite_or_fail := progress ltac:(autorewrite with nat).

#[export] Hint Extern 7 => autorewrite_or_fail : nat.

Proposition strong_induction (P : nat -> Type)
  : (forall n : nat, (forall m : nat,  (m < n) -> P m) -> P n) ->
  forall n : nat, P n.
P: nat -> Type
(forall n : nat, (forall m : nat, m < n -> P m) -> P n) ->
forall n : nat, P n
Proof.
P: nat -> Type
(forall n : nat, (forall m : nat, m < n -> P m) -> P n) ->
forall n : nat, P n
  intro a.
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall n : nat, P n
  assert (forall n m: nat, m < n -> P m) as X.
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall n m : nat, m < n -> P m
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
X: forall n m : nat, m < n -> P m
forall n : nat, P n {
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall n m : nat, m < n -> P m
    simple_induction n n IHn.
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall m : nat, m < 0 -> P m
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
forall m : nat, m < n.+1 -> P m
    -
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall m : nat, m < 0 -> P m intros m l.
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
m: nat
l: m < 0
P m contradiction (not_lt_n_0 m).
    -
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
forall m : nat, m < n.+1 -> P m intros m l.
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
l: m < n.+1
P m apply leq_S_n in l.
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
l: m <= n
P m
      destruct l as [ | n].
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
m: nat
IHn: forall m0 : nat, m0 < m -> P m0
P m
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n.+1 -> P m
m: nat
l: m <= n
P m
      +
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
m: nat
IHn: forall m0 : nat, m0 < m -> P m0
P m apply a; intros ? ?; now apply IHn.
      +
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n.+1 -> P m
m: nat
l: m <= n
P m now apply (IHn m), leq_S_n'.
  }
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
X: forall n m : nat, m < n -> P m
forall n : nat, P n
  intro n.
P: nat -> Type
a: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
X: forall n m : nat, m < n -> P m
n: nat
P n apply (X (n.+1) n), (leq_n n.+1).
Defined.

(** This inductive type is defined because it lets you loop from [i = 0] up to [i = n] by structural induction on a proof of [increasing_geq n 0]. With the existing [leq] type and the inductive structure of [n], it is easier and more natural to loop downwards from [i = n] to [i = 0], but harder to find the least natural number in the interval $[0,n]$ satisfying a given property. *)

Local Unset Elimination Schemes.

Inductive increasing_geq (n : nat) : nat -> Type0 :=
| increasing_geq_n : increasing_geq n n
| increasing_geq_S (m : nat) : increasing_geq n m.+1 ->
                               increasing_geq n m.

Scheme increasing_geq_ind := Induction for increasing_geq Sort Type.
Scheme increasing_geq_rec := Minimality for increasing_geq Sort Type.
Definition increasing_geq_rect := increasing_geq_rec.

Local Set Elimination Schemes.

Proposition increasing_geq_S_n (n m : nat)
  : increasing_geq n m -> increasing_geq n.+1 m.+1.
n, m: nat
increasing_geq n m -> increasing_geq n.+1 m.+1
Proof.
n, m: nat
increasing_geq n m -> increasing_geq n.+1 m.+1
  intro a.
n, m: nat
a: increasing_geq n m
increasing_geq n.+1 m.+1
  induction a.
n: nat
increasing_geq n.+1 n.+1
n, m: nat
a: increasing_geq n m.+1
IHa: increasing_geq n.+1 m.+2
increasing_geq n.+1 m.+1
  -
n: nat
increasing_geq n.+1 n.+1 constructor.
  -
n, m: nat
a: increasing_geq n m.+1
IHa: increasing_geq n.+1 m.+2
increasing_geq n.+1 m.+1 now constructor.
Defined.

Proposition increasing_geq_n_0 (n : nat) : increasing_geq n 0.
n: nat
increasing_geq n 0
Proof.
n: nat
increasing_geq n 0
  simple_induction n n IHn.
increasing_geq 0 0
n: nat
IHn: increasing_geq n 0
increasing_geq n.+1 0
  -
increasing_geq 0 0 constructor.
  -
n: nat
IHn: increasing_geq n 0
increasing_geq n.+1 0 induction IHn.
n: nat
increasing_geq n.+1 n
n, m: nat
IHn: increasing_geq n m.+1
IHIHn: increasing_geq n.+1 m.+1
increasing_geq n.+1 m
    +
n: nat
increasing_geq n.+1 n constructor; now constructor.
    +
n, m: nat
IHn: increasing_geq n m.+1
IHIHn: increasing_geq n.+1 m.+1
increasing_geq n.+1 m constructor; now assumption.
Defined.

Lemma increasing_geq_minus (n k : nat)
  : increasing_geq n (n - k).
n, k: nat
increasing_geq n (n - k)
Proof.
n, k: nat
increasing_geq n (n - k)
  simple_induction k k IHk.
n: nat
increasing_geq n (n - 0)
n, k: nat
IHk: increasing_geq n (n - k)
increasing_geq n (n - k.+1)
  -
n: nat
increasing_geq n (n - 0) destruct (symmetric_paths _ _ (sub_n_0 n)); constructor.
  -
n, k: nat
IHk: increasing_geq n (n - k)
increasing_geq n (n - k.+1) destruct (@leq_dichot n k) as [l | g].
n, k: nat
IHk: increasing_geq n (n - k)
l: n <= k
increasing_geq n (n - k.+1)
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (n - k.+1)
    +
n, k: nat
IHk: increasing_geq n (n - k)
l: n <= k
increasing_geq n (n - k.+1) destruct (symmetric_paths _ _ (sub_leq_0 _ _ _)) in IHk.
n, k: nat
IHk: increasing_geq n 0
l: n <= k
increasing_geq n (n - k.+1)
      apply leq_S in l.
n, k: nat
IHk: increasing_geq n 0
l: n <= k.+1
increasing_geq n (n - k.+1)
      destruct (symmetric_paths _ _ (sub_leq_0 _ _ _)).
n, k: nat
IHk: increasing_geq n 0
l: n <= k.+1
increasing_geq n 0 exact IHk.
    +
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (n - k.+1) change k.+1 with (1 + k).
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (n - (1 + k)) destruct (nat_add_comm k 1).
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (n - (k + 1))
      destruct (symmetric_paths _ _ (subsubadd n k 1)).
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (n - k - 1)
      destruct (symmetric_paths _ _ (@predeqminus1 (n - k))).
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (pred (n - k))
      apply increasing_geq_S.
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (pred (n - k)).+1
      unfold ">", "<" in *.
n, k: nat
IHk: increasing_geq n (n - k)
g: k.+1 <= n
increasing_geq n (pred (n - k)).+1
      apply lt_sub_gt_0 in g.
n, k: nat
IHk: increasing_geq n (n - k)
g: 0 < n - k
increasing_geq n (pred (n - k)).+1 
      now (destruct (symmetric_paths _ _ (S_predn (n - k) 0 _))).
Defined.

Lemma ineq_sub' (n k : nat) : k < n -> n - k = (n - k.+1).+1.
n, k: nat
k < n -> n - k = (n - k.+1).+1
Proof.
n, k: nat
k < n -> n - k = (n - k.+1).+1
  intro ineq.
n, k: nat
ineq: k < n
n - k = (n - k.+1).+1
  destruct n.
k: nat
ineq: k < 0
0 - k = (0 - k.+1).+1
n, k: nat
ineq: k < n.+1
n.+1 - k = (n.+1 - k.+1).+1
  -
k: nat
ineq: k < 0
0 - k = (0 - k.+1).+1 contradiction (not_lt_n_0 k).
  -
n, k: nat
ineq: k < n.+1
n.+1 - k = (n.+1 - k.+1).+1 change (n.+1 - k.+1) with (n - k).
n, k: nat
ineq: k < n.+1
n.+1 - k = (n - k).+1 apply leq_S_n in ineq.
n, k: nat
ineq: k <= n
n.+1 - k = (n - k).+1
    apply (nataddsub_assoc_lemma _).
Defined.

Lemma ineq_sub (n m : nat) : n <= m -> m - (m - n) = n.
n, m: nat
n <= m -> m - (m - n) = n
Proof.
n, m: nat
n <= m -> m - (m - n) = n
  revert m; simple_induction n n IHn.
forall m : nat, 0 <= m -> m - (m - 0) = 0
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
forall m : nat, n.+1 <= m -> m - (m - n.+1) = n.+1
  -
forall m : nat, 0 <= m -> m - (m - 0) = 0 intros.
m: nat
H: 0 <= m
m - (m - 0) = 0 destruct (symmetric_paths _ _ (sub_n_0 m)),
      (symmetric_paths _ _ (sub_n_n m));
      reflexivity.
  -
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
forall m : nat, n.+1 <= m -> m - (m - n.+1) = n.+1 intros m ineq.
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
m - (m - n.+1) = n.+1 change (m - n.+1) with (m - (1 + n)).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
m - (m - (1 + n)) = n.+1
    (destruct (nat_add_comm n 1)).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
m - (m - (n + 1)) = n.+1
    destruct (symmetric_paths _ _ (subsubadd m n 1)).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
m - (m - n - 1) = n.+1 
    destruct (S_predn (m - n) 0 (lt_sub_gt_0 _ _ ineq)); simpl;
      destruct (symmetric_paths _ _ (sub_n_0 (pred (m - n)))).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
m - pred (m - n) = n.+1
    assert (0 < m - n) as dp by exact (lt_sub_gt_0 _ _ ineq).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
dp: 0 < m - n
m - pred (m - n) = n.+1
    assert (pred (m - n) < m) as sh by
        ( unfold "<";
          destruct (symmetric_paths _ _ (S_predn _ 0 _));
          exact sub_less).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
dp: 0 < m - n
sh: pred (m - n) < m
m - pred (m - n) = n.+1
    destruct (symmetric_paths _ _ (ineq_sub' _ _ _)).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
dp: 0 < m - n
sh: pred (m - n) < m
(m - (pred (m - n)).+1).+1 = n.+1
    destruct (symmetric_paths _ _ (S_predn _ 0 _)).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
dp: 0 < m - n
sh: pred (m - n) < m
(m - (m - n)).+1 = n.+1
    apply (ap S), IHn, leq_S', ineq.
Defined.                                 

Proposition leq_equivalent (n m : nat)
  : n <= m <-> increasing_geq m n.
n, m: nat
n <= m <-> increasing_geq m n
Proof.
n, m: nat
n <= m <-> increasing_geq m n
  split.
n, m: nat
n <= m -> increasing_geq m n
n, m: nat
increasing_geq m n -> n <= m
  -
n, m: nat
n <= m -> increasing_geq m n intro ineq.
n, m: nat
ineq: n <= m
increasing_geq m n induction ineq.
n: nat
increasing_geq n n
n, m: nat
ineq: n <= m
IHineq: increasing_geq m n
increasing_geq m.+1 n
    +
n: nat
increasing_geq n n constructor.
    +
n, m: nat
ineq: n <= m
IHineq: increasing_geq m n
increasing_geq m.+1 n apply increasing_geq_S_n in IHineq; constructor; assumption.
  -
n, m: nat
increasing_geq m n -> n <= m intro a.
n, m: nat
a: increasing_geq m n
n <= m
    induction a.
m: nat
m <= m
m, m0: nat
a: increasing_geq m m0.+1
IHa: m0.+1 <= m
m0 <= m
    +
m: nat
m <= m constructor.
    +
m, m0: nat
a: increasing_geq m m0.+1
IHa: m0.+1 <= m
m0 <= m exact (leq_S' _ _ _).
Defined.

(** This tautology accepts a (potentially opaqued or QED'ed) proof of [n <= m], and returns a transparent proof which can be computed with (i.e., one can loop from n to m) *) 
Definition leq_wrapper {n m : nat} : n <= m -> n <= m.
n, m: nat
n <= m -> n <= m
Proof.
n, m: nat
n <= m -> n <= m
  intro ineq.
n, m: nat
ineq: n <= m
n <= m
  destruct (@leq_dichot n m) as [l | g].
n, m: nat
ineq, l: n <= m
n <= m
n, m: nat
ineq: n <= m
g: n > m
n <= m
  -
n, m: nat
ineq, l: n <= m
n <= m exact l.
  -
n, m: nat
ineq: n <= m
g: n > m
n <= m contradiction (not_lt_n_n m (@mixed_trans2 _ _ _ g ineq)).
Defined.

Proposition symmetric_rel_total_order (R : nat -> nat -> Type)
            {p : Symmetric R} {p' : Reflexive R}
  : (forall n m : nat, n < m -> R n m) -> (forall n m : nat, R n m).
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
(forall n m : nat, n < m -> R n m) ->
forall n m : nat, R n m
Proof.
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
(forall n m : nat, n < m -> R n m) ->
forall n m : nat, R n m
  intros A n m.
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
n, m: nat
R n m
  destruct (@leq_dichot m n) as [m_leq_n | m_gt_n].
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
n, m: nat
m_leq_n: m <= n
R n m
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
n, m: nat
m_gt_n: m > n
R n m
  -
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
n, m: nat
m_leq_n: m <= n
R n m apply symmetry.
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
n, m: nat
m_leq_n: m <= n
R m n destruct m_leq_n.
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
m: nat
R m m
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
m, m0: nat
m_leq_n: m <= m0
R m m0.+1
    +
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
m: nat
R m m apply reflexivity.
    +
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
m, m0: nat
m_leq_n: m <= m0
R m m0.+1 apply A.
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
m, m0: nat
m_leq_n: m <= m0
m < m0.+1 apply leq_S_n'.
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
m, m0: nat
m_leq_n: m <= m0
m <= m0 assumption.
  -
R: nat -> nat -> Type
p: Symmetric R
p': Reflexive R
A: forall n m : nat, n < m -> R n m
n, m: nat
m_gt_n: m > n
R n m apply A, m_gt_n.
Defined.