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.

(** TODO: The results in this file are in the process of being moved over to Core.v *)

(** TODO: move, rename *)
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; exact _. 
  -
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_refl.
    +
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.

(** TODO: move, rename *)
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 (nat_add_zero_r n)^, (nat_add_zero_r (n - m))^; constructor.
  -
n, m, k: nat
IHk: n + k - m <= n - m + k
n + k.+1 - m <= n - m + k.+1 destruct (nat_add_succ_r 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 (nat_add_succ_r (n - m) k)^.
n, m, k: nat
IHk: n + k - m <= n - m + k
(n + k - m).+1 <= (n - m + k).+1
    by apply leq_succ.
Defined.

(** TODO: move, rename *)
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_dichotomy 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 rewrite <- nat_sub_l_add_l; trivial.
n, m: nat
l: m <= n
n <= n + m - m
    destruct (nat_add_sub_cancel_r 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 leq_lt in gt.
n, m: nat
gt: n <= m
n <= n - m + m
    destruct (equiv_nat_sub_leq _)^.
n, m: nat
gt: n <= m
n <= 0 + m
    assumption.
Defined.

(** TODO: move, rename *)
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_zero_r _ _).
  -
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_zero_l.
    +
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_succ.
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 exact (IHn m i l).
Defined.

(** TODO: move, rename *)
Proposition predeqminus1 { n : nat } : n - 1 = nat_pred n.
n: nat
n - 1 = nat_pred n
Proof.
n: nat
n - 1 = nat_pred n
  simple_induction' n.
0 - 1 = nat_pred 0
n: nat
IH: n - 1 = nat_pred n
n.+1 - 1 = nat_pred n.+1
  -
0 - 1 = nat_pred 0 reflexivity.
  -
n: nat
IH: n - 1 = nat_pred n
n.+1 - 1 = nat_pred n.+1 apply nat_sub_zero_r.
Defined.

(** TODO: move, rename *)
Proposition predn_leq_n (n : nat) : nat_pred n <= n.
n: nat
nat_pred n <= n
Proof.
n: nat
nat_pred n <= n
  destruct n; exact _.
Defined.

(** TODO: move, rename *)
Proposition pred_equiv (k n : nat) : k < n -> k < S (nat_pred n).
k, n: nat
k < n -> k < (nat_pred n).+1
Proof.
k, n: nat
k < n -> k < (nat_pred n).+1 
  intro ineq; destruct n.
k: nat
ineq: k < 0
k < (nat_pred 0).+1
k, n: nat
ineq: k < n.+1
k < (nat_pred n.+1).+1
  -
k: nat
ineq: k < 0
k < (nat_pred 0).+1 contradiction (not_lt_zero_r _ _).
  -
k, n: nat
ineq: k < n.+1
k < (nat_pred n.+1).+1 assumption.
Defined.

(** TODO: move, rename *)
Proposition n_leq_pred_Sn (n : nat) : n <= S (nat_pred n).
n: nat
n <= (nat_pred n).+1
Proof.
n: nat
n <= (nat_pred n).+1 
  destruct n; exact _.
Defined.

(** TODO: move, rename *)
Proposition leq_implies_pred_lt (i n k : nat)
  : (n > i) -> n <= k -> nat_pred n < k.
i, n, k: nat
n > i -> n <= k -> nat_pred n < k
Proof.
i, n, k: nat
n > i -> n <= k -> nat_pred n < k
  intro ineq; destruct n.
i, k: nat
ineq: 0 > i
0 <= k -> nat_pred 0 < k
i, n, k: nat
ineq: n.+1 > i
n.+1 <= k -> nat_pred n.+1 < k
  -
i, k: nat
ineq: 0 > i
0 <= k -> nat_pred 0 < k contradiction (not_lt_zero_r i).
  -
i, n, k: nat
ineq: n.+1 > i
n.+1 <= k -> nat_pred n.+1 < k intro; assumption.
Defined.

(** TODO: move, rename *)
Proposition pred_lt_implies_leq (n k : nat)
  : nat_pred n < k -> n <= k.
n, k: nat
nat_pred n < k -> n <= k
Proof.
n, k: nat
nat_pred n < k -> n <= k
  intro l; destruct n.
k: nat
l: nat_pred 0 < k
0 <= k
n, k: nat
l: nat_pred n.+1 < k
n.+1 <= k
  -
k: nat
l: nat_pred 0 < k
0 <= k apply leq_zero_l.
  -
n, k: nat
l: nat_pred n.+1 < k
n.+1 <= k assumption.
Defined.

(** TODO: move, rename *)
Proposition lt_implies_pred_geq (i j : nat) : i < j -> i <= nat_pred j.
i, j: nat
i < j -> i <= nat_pred j
Proof.
i, j: nat
i < j -> i <= nat_pred j
  intro l; apply leq_pred in l; assumption.
Defined.

(** TODO: move, rename *)
Proposition j_geq_0_lt_implies_pred_geq (i j k : nat)
  : i < j -> k.+1 <= j -> k <= nat_pred j.
i, j, k: nat
i < j -> k.+1 <= j -> k <= nat_pred j
Proof.
i, j, k: nat
i < j -> k.+1 <= j -> k <= nat_pred j
  intros l ineq.
i, j, k: nat
l: i < j
ineq: k.+1 <= j
k <= nat_pred j
  destruct j.
i, k: nat
l: i < 0
ineq: k.+1 <= 0
k <= nat_pred 0
i, j, k: nat
l: i < j.+1
ineq: k.+1 <= j.+1
k <= nat_pred j.+1
  -
i, k: nat
l: i < 0
ineq: k.+1 <= 0
k <= nat_pred 0 contradiction (not_lt_zero_r i).
  -
i, j, k: nat
l: i < j.+1
ineq: k.+1 <= j.+1
k <= nat_pred j.+1 by simpl; apply leq_pred'.
Defined.

(** TODO: move, rename *)
Proposition pred_gt_implies_lt (i j : nat)
  : i < nat_pred j -> i.+1 < j.
i, j: nat
i < nat_pred j -> i.+1 < j
Proof.
i, j: nat
i < nat_pred j -> i.+1 < j
  intros ineq.
i, j: nat
ineq: i < nat_pred j
i.+1 < j
  assert (H := leq_succ ineq).
i, j: nat
ineq: i < nat_pred j
H: i.+2 <= (nat_pred j).+1
i.+1 < j assert (i < j) as X.
i, j: nat
ineq: i < nat_pred j
H: i.+2 <= (nat_pred j).+1
i < j
i, j: nat
ineq: i < nat_pred j
H: i.+2 <= (nat_pred j).+1
X: i < j
i.+1 < j {
i, j: nat
ineq: i < nat_pred j
H: i.+2 <= (nat_pred j).+1
i < j
    apply (@lt_lt_leq_trans _ (nat_pred j) _);
      [assumption  | apply predn_leq_n].
  }
i, j: nat
ineq: i < nat_pred j
H: i.+2 <= (nat_pred j).+1
X: i < j
i.+1 < j
  by rewrite <- (nat_succ_pred' j i).
Defined.

(** TODO: move, rename *)
Proposition pred_preserves_lt {i n: nat} (p : i < n) m
  : (n < m) -> (nat_pred n < nat_pred m).
i, n: nat
p: i < n
m: nat
n < m -> nat_pred n < nat_pred m
Proof.
i, n: nat
p: i < n
m: nat
n < m -> nat_pred n < nat_pred m
  intro l.
i, n: nat
p: i < n
m: nat
l: n < m
nat_pred n < nat_pred m
  apply leq_pred'.
i, n: nat
p: i < n
m: nat
l: n < m
(nat_pred n).+2 <= (nat_pred m).+1 destruct (symmetric_paths _ _ (nat_succ_pred' n i _)).
i, n: nat
p: i < n
m: nat
l: n < m
n.+1 <= (nat_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 <= (nat_pred m).+1
  destruct (symmetric_paths _ _ (nat_succ_pred' 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.

(** TODO: move, rename *)
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_zero_l.
  -
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_refl.
    +
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_succ_r, leq_refl].
Defined.

(** TODO: move, rename *)
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_zero_r _ _)).
n, k: nat
l: 0 < n.+1
l': 0 < k.+1
(n.+1 - k.+1).+1 <= n.+1
  simpl; apply leq_succ, sub_less.
Defined.

(** TODO: move, rename *)
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 (leq_add_r m k).
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 by 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; by constructor.
    +
n, m: nat
IHn: increasing_geq n m.+1
IHIHn: increasing_geq n.+1 m.+1
increasing_geq n.+1 m constructor; by 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 _ _ (nat_sub_zero_r n)); constructor.
  -
n, k: nat
IHk: increasing_geq n (n - k)
increasing_geq n (n - k.+1) destruct (@leq_dichotomy 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 (equiv_nat_sub_leq _)^ in IHk.
n, k: nat
IHk: increasing_geq n 0
l: n <= k
increasing_geq n (n - k.+1)
      apply leq_succ_r in l.
n, k: nat
IHk: increasing_geq n 0
l: n <= k.+1
increasing_geq n (n - k.+1)
      destruct (equiv_nat_sub_leq _)^.
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 _ _ (nat_sub_r_add 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 (nat_pred (n - k))
      apply increasing_geq_S.
n, k: nat
IHk: increasing_geq n (n - k)
g: n > k
increasing_geq n (nat_pred (n - k)).+1
      unfold ">", "<" in *.
n, k: nat
IHk: increasing_geq n (n - k)
g: k.+1 <= n
increasing_geq n (nat_pred (n - k)).+1
      apply equiv_lt_lt_sub in g.
n, k: nat
IHk: increasing_geq n (n - k)
g: 0 < n - k
increasing_geq n (nat_pred (n - k)).+1 
      by (destruct (symmetric_paths _ _ (nat_succ_pred (n - k) _))).
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_zero_r 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_pred' in ineq.
n, k: nat
ineq: k <= n
n.+1 - k = (n - k).+1
    by apply nat_sub_succ_l.
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 _ _ (nat_sub_zero_r m)),
      (symmetric_paths _ _ (nat_sub_cancel 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 _ _ (nat_sub_r_add 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 (nat_succ_pred (m - n) (equiv_lt_lt_sub _ _ ineq)); simpl;
      destruct (symmetric_paths _ _ (nat_sub_zero_r (nat_pred (m - n)))).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
m - nat_pred (m - n) = n.+1
    assert (0 < m - n) as dp by exact (equiv_lt_lt_sub _ _ ineq).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
dp: 0 < m - n
m - nat_pred (m - n) = n.+1
    assert (nat_pred (m - n) < m) as sh by
        ( unfold "<";
          destruct (symmetric_paths _ _ (nat_succ_pred _ _));
          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: nat_pred (m - n) < m
m - nat_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: nat_pred (m - n) < m
(m - (nat_pred (m - n)).+1).+1 = n.+1
    destruct (symmetric_paths _ _ (nat_succ_pred _ _)).
n: nat
IHn: forall m : nat, n <= m -> m - (m - n) = n
m: nat
ineq: n.+1 <= m
dp: 0 < m - n
sh: nat_pred (m - n) < m
(m - (m - n)).+1 = n.+1
    apply (ap S), IHn, leq_succ_l, 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_succ_l _).
Defined.

(** TODO: remove *)
(** 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_dichotomy 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 (lt_irrefl m (lt_lt_leq_trans 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_dichotomy 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_succ.
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.