(******************************************************************************)
(*                                                                            *)
(*                              Triangular number                             *)
(*                                                                            *)
(******************************************************************************)
(*                                                                            *)
(*     delta n = the n^th triangular number                                   *)
(*     troot n = the triangular root of n                                     *)
(*      tmod n = the triangular modulo of n                                   *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

From mathcomp Require Import all_ssreflect.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma prednDl m n : 0 < m -> (m + n).-1 = m.-1 + n.
m, n:nat
0 < m -> (m + n).-1 = m.-1 + n
Proof.
m, n:nat
0 < m -> (m + n).-1 = m.-1 + n by case: m. Qed.

Lemma prednDr m n : 0 < n -> (m + n).-1 = m + n.-1.
m, n:nat
0 < n -> (m + n).-1 = m + n.-1
Proof.
m, n:nat
0 < n -> (m + n).-1 = m + n.-1 by case: n => // n; rewrite addnS. Qed.

Lemma leq_sub_sub a b c : ((a - b) - (c - b)) <= a - c.
a, b, c:nat
a - b - (c - b) <= a - c
Proof.
a, b, c:nat
a - b - (c - b) <= a - c
have [aLb|bLa] := leqP b a; last first.
a, b, c:nat
bLa:a < b
a - b - (c - b) <= a - c
a, b, c:nat
aLb:b <= a
a - b - (c - b) <= a - c
  rewrite (_ : a - _ = 0) ?sub0n //.
a, b, c:nat
bLa:a < b
a - b = 0
a, b, c:nat
aLb:b <= a
a - b - (c - b) <= a - c
  by apply/eqP; rewrite subn_eq0 ltnW.
a, b, c:nat
aLb:b <= a
a - b - (c - b) <= a - c
have [cLb|bLc] := leqP c b; last first.
a, b, c:nat
aLb:b <= a
bLc:b < c
a - b - (c - b) <= a - c
a, b, c:nat
aLb:b <= a
cLb:c <= b
a - b - (c - b) <= a - c
  by rewrite subnBA ?subnK // ltnW.
a, b, c:nat
aLb:b <= a
cLb:c <= b
a - b - (c - b) <= a - c
rewrite (_ : c - _ = 0); last by apply/eqP; rewrite subn_eq0.
a, b, c:nat
aLb:b <= a
cLb:c <= b
a - b - 0 <= a - c
by rewrite subn0 leq_sub2l.
Qed.

Lemma leq_sub_add b a c : a - c <= (a - b) + (b - c).
b, a, c:nat
a - c <= a - b + (b - c)
Proof.
b, a, c:nat
a - c <= a - b + (b - c)
rewrite leq_subLR addnC -addnA.
b, a, c:nat
a <= a - b + (b - c + c)
have [/subnK->|H] := leqP c b.
b, a, c:nat
a <= a - b + b
b, a, c:nat
H:b < c
a <= a - b + (b - c + c)
  have [/subnK->//|H] := leqP b a.
b, a, c:nat
H:a < b
a <= a - b + b
b, a, c:nat
H:b < c
a <= a - b + (b - c + c)
  apply: leq_trans (ltnW H) _.
b, a, c:nat
H:a < b
b <= a - b + b
b, a, c:nat
H:b < c
a <= a - b + (b - c + c)
  by apply: leq_addl.
b, a, c:nat
H:b < c
a <= a - b + (b - c + c)
have := ltnW H.
b, a, c:nat
H:b < c
b <= c -> a <= a - b + (b - c + c)
rewrite -subn_eq0 => /eqP->.
b, a, c:nat
H:b < c
a <= a - b + (0 + c)
rewrite addnC -leq_subLR.
b, a, c:nat
H:b < c
a - (0 + c) <= a - b
by apply: leq_sub2l; apply: ltnW.
Qed.

(******************************************************************************)
(*                                                                            *)
(*                               Triangular number                            *)
(*                                                                            *)
(******************************************************************************)

Definition delta n := (n.+1 * n)./2.

Notation "'Δ' n " := (delta n) (format "'Δ' n", at level 10).

Compute zip (iota 1 20) (map delta (iota 1 20)).
= [:: (1, 1); (2, 3); (3, 6); (4, 10); (5, 15);
      (6, 21); (7, 28); (8, 36); (9, 45);
      (10, 55); (11, 66); (12, 78); (13, 91);
      (14, 105); (15, 120); (16, 136); (17, 153);
      (18, 171); (19, 190); (20, 210)]
: seq (nat * nat)

Lemma deltaS n : delta n.+1 = delta n + n.+1.
n:nat
Δn.+1 = Δn + n.+1
Proof.
n:nat
Δn.+1 = Δn + n.+1
rewrite /delta -addn2 mulnDl mulnC halfD.
n:nat
odd (n.+1 * n) && odd (2 * n.+1) +
((n.+1 * n)./2 + (2 * n.+1)./2) = (n.+1 * n)./2 + n.+1
rewrite !oddM andbF add0n mul2n.
n:nat
(n.+1 * n)./2 + ((n.+1).*2)./2 = (n.+1 * n)./2 + n.+1
by rewrite -{4}(half_bit_double n.+1 false).
Qed.

Lemma delta_gt0 n : 0 < n -> 0 < delta n.
n:nat
0 < n -> 0 < Δn
Proof.
n:nat
0 < n -> 0 < Δn by case: n => // n _; rewrite deltaS addnS ltnS leq_addr. Qed.

Lemma deltaE n : delta n = \sum_(i < n.+1) i.
n:nat
Δn = \sum_(i < n.+1) i
Proof.
n:nat
Δn = \sum_(i < n.+1) i
elim: n => [|n IH]; first by rewrite big_ord_recl big_ord0.
n:nat
IH:Δn = \sum_(i < n.+1) i
Δn.+1 = \sum_(i < n.+2) i
by rewrite big_ord_recr /= -IH deltaS.
Qed.

Compute zip (iota 0 11) (map delta (iota 0 11)).
= [:: (0, 0); (1, 1); (2, 3); (3, 6); (4, 10);
      (5, 15); (6, 21); (7, 28); (8, 36);
      (9, 45); (10, 55)]
: seq (nat * nat)

Lemma delta_le m n : m <= n -> delta m <= delta n.
m, n:nat
m <= n -> Δm <= Δn
Proof.
m, n:nat
m <= n -> Δm <= Δn by move=> H; apply/half_leq/leq_mul. Qed.

Lemma delta_square n : (8 * delta n).+1 = n.*2.+1 ^ 2.
n:nat
(8 * Δn).+1 = n.*2.+1 ^ 2
Proof.
n:nat
(8 * Δn).+1 = n.*2.+1 ^ 2
elim: n => // n IH.
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
(8 * Δn.+1).+1 = (n.+1).*2.+1 ^ 2
rewrite deltaS mulnDr -addSn IH.
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
n.*2.+1 ^ 2 + 8 * n.+1 = (n.+1).*2.+1 ^ 2
rewrite doubleS -addn1 -addnS -addSn addn1.
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
n.*2.+1 ^ 2 + 8 * n.+1 = (n.*2.+1 + 2) ^ 2
rewrite sqrnD -addnA /=.
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
n.*2.+1 ^ 2 + 8 * n.+1 =
n.*2.+1 ^ 2 + (2 ^ 2 + 2 * (n.*2.+1 * 2))
congr (_ + _).
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
8 * n.+1 = 2 ^ 2 + 2 * (n.*2.+1 * 2)
rewrite mulnS.
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
8 + 8 * n = 2 ^ 2 + 2 * (n.*2.+1 * 2)
rewrite [_ * 2]mulSn mulnDr addnA.
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
8 + 8 * n = 2 ^ 2 + 2 * 2 + 2 * (n.*2 * 2)
congr (_ + _).
n:nat
IH:(8 * Δn).+1 = n.*2.+1 ^ 2
8 * n = 2 * (n.*2 * 2)
by rewrite mulnCA -muln2 -!mulnA mulnC.
Qed.

Lemma geq_deltann n : n <= delta n.
n:nat
n <= Δn
Proof.
n:nat
n <= Δn
by case: n => // n; rewrite deltaS addnS ltnS leq_addl.
Qed.

(******************************************************************************)
(*                                                                            *)
(*                               Triangular root                              *)
(*                                                                            *)
(******************************************************************************)

Definition troot n := 
 let l := iota 0 n.+2 in
 (find (fun x => n < delta x) l).-1.

Notation "∇ n" := (troot n) (format "∇ n", at level 10).

Compute zip (iota 0 11) (map troot (iota 0 11)).
= [:: (0, 0); (1, 1); (2, 1); (3, 2); (4, 2);
      (5, 2); (6, 3); (7, 3); (8, 3); (9, 3);
      (10, 4)]
: seq (nat * nat)

Lemma troot_gt0 n : 0 < n -> 0 < troot n.
n:nat
0 < n -> 0 < ∇n
Proof.
n:nat
0 < n -> 0 < ∇n by case: n. Qed.

Lemma delta_root_le m : delta (troot m) <= m.
m:nat
Δ(∇m) <= m
Proof.
m:nat
Δ(∇m) <= m
rewrite /troot leqNgt.
m:nat
~~
(m < Δ(find (fun x : nat => m < Δx) (iota 0 m.+2)).-1)
set l := iota _ _; set f := (fun _ => _).
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
~~ (m < Δ(find f l).-1)
case E : _.-1 => [|n] //.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
n:nat
E:(find f l).-1 = n.+1
~~ (m < Δn.+1)
have  /(before_find 0) : 
   (find f l).-1 < find f l by rewrite prednK // E.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
n:nat
E:(find f l).-1 = n.+1
f (nth 0 l (find f l).-1) = false -> ~~ (m < Δn.+1)
rewrite E  nth_iota // /f => [->//|].
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
n:nat
E:(find f l).-1 = n.+1
n.+1 < m.+2
rewrite -[m.+2](size_iota 0) -E prednK; first by apply: find_size.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
n:nat
E:(find f l).-1 = n.+1
0 < find f l
by case: find E.
Qed.

Lemma delta_root_gt m : m < delta (troot m).+1.
m:nat
m < Δ(∇m).+1
Proof.
m:nat
m < Δ(∇m).+1
rewrite /troot leqNgt.
m:nat
~~
(Δ(find (fun x : nat => m < Δx) (iota 0 m.+2)).-1.+1 <
 m.+1)
set l := iota _ _; set f := (fun _ => _).
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
~~ (Δ(find f l).-1.+1 < m.+1)
have Hfl : has f l.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
has f l
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
~~ (Δ(find f l).-1.+1 < m.+1)
  apply/hasP; exists m.+1; first by rewrite mem_iota leq0n leqnn.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
f m.+1
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
~~ (Δ(find f l).-1.+1 < m.+1)
  rewrite /f /delta -{1}[m.+1](half_bit_double _ false).
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
(false + (m.+1).*2)./2 <= (m.+2 * m.+1)./2
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
~~ (Δ(find f l).-1.+1 < m.+1)
  by apply/half_leq; rewrite add0n -mul2n leq_mul2r orbT.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
~~ (Δ(find f l).-1.+1 < m.+1)
have := nth_find 0 Hfl; rewrite {1}/f.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
m < Δ(nth 0 l (find f l)) ->
~~ (Δ(find f l).-1.+1 < m.+1)
case E : _.-1 => [|n] //.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
E:(find f l).-1 = 0
m < Δ(nth 0 l (find f l)) -> ~~ (Δ1 < m.+1)
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
n:nat
E:(find f l).-1 = n.+1
m < Δ(nth 0 l (find f l)) -> ~~ (Δn.+2 < m.+1)
  case: find E => // [] [|n] //.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
1.-1 = 0 -> m < Δ(nth 0 l 1) -> ~~ (Δ1 < m.+1)
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
n:nat
E:(find f l).-1 = n.+1
m < Δ(nth 0 l (find f l)) -> ~~ (Δn.+2 < m.+1)
  by rewrite nth_iota //=; case: (m).
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
n:nat
E:(find f l).-1 = n.+1
m < Δ(nth 0 l (find f l)) -> ~~ (Δn.+2 < m.+1)
rewrite nth_iota.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
n:nat
E:(find f l).-1 = n.+1
m < Δ(0 + find f l) -> ~~ (Δn.+2 < m.+1)
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
n:nat
E:(find f l).-1 = n.+1
find f l < m.+2
  by rewrite -E prednK // ltnNge ltnS.
m:nat
l:=iota 0 m.+2:seq nat
f:=fun H : nat => m < ΔH:nat -> bool
Hfl:has f l
n:nat
E:(find f l).-1 = n.+1
find f l < m.+2
by rewrite -(size_iota 0 m.+2) -has_find.
Qed.

(* Galois connection *)
Lemma root_delta_le m n : (n <= troot m) = (delta n <= m).
m, n:nat
(n <= ∇m) = (Δn <= m)
Proof.
m, n:nat
(n <= ∇m) = (Δn <= m)
case: leqP => [/delta_le/leq_trans->//|dmLn].
m, n:nat
Δ(∇m) <= m
m, n:nat
dmLn:∇m < n
false = (Δn <= m)
  apply: delta_root_le.
m, n:nat
dmLn:∇m < n
false = (Δn <= m)
apply/sym_equal/idP/negP.
m, n:nat
dmLn:∇m < n
~~ (Δn <= m)
rewrite -ltnNge.
m, n:nat
dmLn:∇m < n
m < Δn
by apply: leq_trans (delta_root_gt _) (delta_le dmLn).
Qed.

Lemma root_delta_lt m n : (troot m < n) = (m < delta n).
m, n:nat
(∇m < n) = (m < Δn)
Proof.
m, n:nat
(∇m < n) = (m < Δn) by rewrite ltnNge root_delta_le -ltnNge. Qed.

Lemma troot_le m n : m <= n -> troot m <= troot n.
m, n:nat
m <= n -> ∇m <= ∇n
Proof.
m, n:nat
m <= n -> ∇m <= ∇n
by move=> mLn; rewrite root_delta_le (leq_trans (delta_root_le _)).
Qed.

Lemma trootE m n : (troot m == n) = (delta n <= m < delta n.+1).
m:nat
n:nat_eqType
(∇m == n) = (Δn <= m < Δn.+1)
Proof.
m:nat
n:nat_eqType
(∇m == n) = (Δn <= m < Δn.+1)
rewrite ltnNge -!root_delta_le -ltnNge.
m:nat
n:nat_eqType
(∇m == n) = (n <= ∇m < n.+1)
by rewrite ltnS -eqn_leq.
Qed.

Lemma troot_delta n : troot (delta n) = n.
n:nat
∇(Δn) = n
Proof.
n:nat
∇(Δn) = n by apply/eqP; rewrite trootE leqnn deltaS -addn1 leq_add2l. Qed.

Lemma leq_rootnn n : troot n <= n.
n:nat
∇n <= n
Proof.
n:nat
∇n <= n
by rewrite -{2}[n]troot_delta troot_le // geq_deltann.
Qed.

(******************************************************************************)
(*                                                                            *)
(*                               Triangular modulo                            *)
(*                                                                            *)
(******************************************************************************)

Definition tmod n := n - delta (troot n).

Lemma tmod_delta n : tmod (delta n) = 0.
n:nat
tmod (Δn) = 0
Proof.
n:nat
tmod (Δn) = 0 by rewrite /tmod troot_delta subnn. Qed.

Lemma tmodE n : n = delta (troot n) + tmod n.
n:nat
n = Δ(∇n) + tmod n
Proof.
n:nat
n = Δ(∇n) + tmod n by rewrite addnC (subnK (delta_root_le _)). Qed.

Lemma tmod_le n : tmod n <= troot n.
n:nat
tmod n <= ∇n
Proof.
n:nat
tmod n <= ∇n  by rewrite leq_subLR -ltnS -addnS -deltaS delta_root_gt. Qed.


Lemma ltn_root m n : troot m < troot n -> m < n.
m, n:nat
∇m < ∇n -> m < n
Proof.
m, n:nat
∇m < ∇n -> m < n
rewrite root_delta_le deltaS => /(leq_trans _) -> //.
m, n:nat
m < Δ(∇m) + (∇m).+1
by rewrite {1}[m]tmodE ltn_add2l ltnS tmod_le.
Qed.

Lemma leq_mod m n : troot m = troot n -> (tmod m <= tmod n) = (m <= n).
m, n:nat
∇m = ∇n -> (tmod m <= tmod n) = (m <= n)
Proof.
m, n:nat
∇m = ∇n -> (tmod m <= tmod n) = (m <= n)
by move=> tmEtn; rewrite {2}[m]tmodE {2}[n]tmodE tmEtn leq_add2l.
Qed.

Lemma ltn_mod m n : troot m = troot n -> (tmod m < tmod n) = (m < n).
m, n:nat
∇m = ∇n -> (tmod m < tmod n) = (m < n)
Proof.
m, n:nat
∇m = ∇n -> (tmod m < tmod n) = (m < n)
by move=> tmEtn; rewrite {2}[m]tmodE {2}[n]tmodE tmEtn ltn_add2l.
Qed.

Lemma troot_mod_case m : 
         ((troot m.+1 == troot m) && (tmod m.+1 == (tmod m).+1))
      || 
         [&& troot m.+1 == (troot m).+1, tmod m.+1 == 0 & tmod m == troot m].
m:nat
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m]
Proof.
m:nat
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m]
have := troot_le (leqnSn m).
m:nat
∇m <= ∇m.+1 ->
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m]
rewrite leq_eqVlt => /orP[/eqP He|He].
m:nat
He:∇m = ∇m.+1
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m]
m:nat
He:∇m < ∇m.+1
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m]
  by rewrite /tmod -He subSn ?eqxx // {2}[m]tmodE leq_addr.
m:nat
He:∇m < ∇m.+1
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m]
rewrite orbC.
m:nat
He:∇m < ∇m.+1
[&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0 & tmod m == ∇m]
|| (∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
have: troot m.+1 == (troot m).+1.
m:nat
He:∇m < ∇m.+1
∇m.+1 == (∇m).+1
m:nat
He:∇m < ∇m.+1
∇m.+1 == (∇m).+1 ->
[&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0 & tmod m == ∇m]
|| (∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
  rewrite trootE (leq_trans (delta_le He)) //; last first.
m:nat
He:∇m < ∇m.+1
Δ(∇m.+1) <= m.+1
m:nat
He:∇m < ∇m.+1
true && (m.+1 < Δ(∇m).+2)
m:nat
He:∇m < ∇m.+1
∇m.+1 == (∇m).+1 ->
[&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0 & tmod m == ∇m]
|| (∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
    by rewrite {2}[m.+1]tmodE leq_addr.
m:nat
He:∇m < ∇m.+1
true && (m.+1 < Δ(∇m).+2)
m:nat
He:∇m < ∇m.+1
∇m.+1 == (∇m).+1 ->
[&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0 & tmod m == ∇m]
|| (∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
  rewrite !deltaS {1}[m]tmodE -addnS -addnS -addnA.
m:nat
He:∇m < ∇m.+1
true &&
(Δ(∇m) + (tmod m).+2 <= Δ(∇m) + ((∇m).+1 + (∇m).+2))
m:nat
He:∇m < ∇m.+1
∇m.+1 == (∇m).+1 ->
[&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0 & tmod m == ∇m]
|| (∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
  by rewrite leq_add2l (leq_trans _ (leq_addl _ _)) // !ltnS tmod_le.
m:nat
He:∇m < ∇m.+1
∇m.+1 == (∇m).+1 ->
[&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0 & tmod m == ∇m]
|| (∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
move/eqP=> He1.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
[&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0 & tmod m == ∇m]
|| (∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
rewrite He1 eqxx.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
have := eqxx m.+1.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
m.+1 == m.+1 ->
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
rewrite {1}[m]tmodE {1}[m.+1]tmodE He1 deltaS -addnS.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
Δ(∇m) + (tmod m).+1 == Δ(∇m) + (∇m).+1 + tmod m.+1 ->
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
rewrite -!addnA eqn_add2l addSn eqSS => /eqP He2.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
He2:tmod m = ∇m + tmod m.+1
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
have := tmod_le m.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
He2:tmod m = ∇m + tmod m.+1
tmod m <= ∇m ->
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
rewrite leq_eqVlt => /orP[/eqP He3|]; last first.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
He2:tmod m = ∇m + tmod m.+1
tmod m < ∇m ->
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
He2:tmod m = ∇m + tmod m.+1
He3:tmod m = ∇m
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
  by rewrite He2 ltnNge leq_addr.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
He2:tmod m = ∇m + tmod m.+1
He3:tmod m = ∇m
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
rewrite He3 -(eqn_add2l (tmod m)) {1}He3 -He2 addn0.
m:nat
He:∇m < ∇m.+1
He1:∇m.+1 = (∇m).+1
He2:tmod m = ∇m + tmod m.+1
He3:tmod m = ∇m
[&& true, tmod m == tmod m & ∇m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (∇m).+1)
by rewrite !eqxx.
Qed.

Lemma troot_mod_le m n : 
   m <= n = 
   ((troot m < troot n) || ((troot m == troot n) && (tmod m <= tmod n))).
m, n:nat
(m <= n) =
(∇m < ∇n) || (∇m == ∇n) && (tmod m <= tmod n)
Proof.
m, n:nat
(m <= n) =
(∇m < ∇n) || (∇m == ∇n) && (tmod m <= tmod n)
case: leqP => [|dmGdn] /= ; last first.
m, n:nat
dmGdn:∇m < ∇n
(m <= n) = true
m, n:nat
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
  apply/idP.
m, n:nat
dmGdn:∇m < ∇n
m <= n
m, n:nat
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
  apply: (leq_trans (_ : _ <= delta (troot m).+1)).
m, n:nat
dmGdn:∇m < ∇n
m <= Δ(∇m).+1
m, n:nat
dmGdn:∇m < ∇n
Δ(∇m).+1 <= n
m, n:nat
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
    by rewrite ltnW // delta_root_gt.
m, n:nat
dmGdn:∇m < ∇n
Δ(∇m).+1 <= n
m, n:nat
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
  apply: (leq_trans (_ : _ <= delta (troot n))).
m, n:nat
dmGdn:∇m < ∇n
Δ(∇m).+1 <= Δ(∇n)
m, n:nat
dmGdn:∇m < ∇n
Δ(∇n) <= n
m, n:nat
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
    by apply: delta_le.
m, n:nat
dmGdn:∇m < ∇n
Δ(∇n) <= n
m, n:nat
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
  by apply: delta_root_le.
m, n:nat
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
rewrite leq_eqVlt => /orP[/eqP dnEdm|dmLdn].
m, n:nat
dnEdm:∇n = ∇m
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
m, n:nat
dmLdn:∇n < ∇m
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
  rewrite dnEdm eqxx /=.
m, n:nat
dnEdm:∇n = ∇m
(m <= n) = (tmod m <= tmod n)
m, n:nat
dmLdn:∇n < ∇m
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
  by rewrite {1}[m]tmodE {1}[n]tmodE dnEdm leq_add2l.
m, n:nat
dmLdn:∇n < ∇m
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
rewrite (gtn_eqF dmLdn) /=.
m, n:nat
dmLdn:∇n < ∇m
(m <= n) = false
apply/idP/negP.
m, n:nat
dmLdn:∇n < ∇m
~~ (m <= n)
rewrite -ltnNge.
m, n:nat
dmLdn:∇n < ∇m
n < m
apply: (leq_trans (delta_root_gt _)).
m, n:nat
dmLdn:∇n < ∇m
Δ(∇n).+1 <= m
apply: (leq_trans _ (delta_root_le _)).
m, n:nat
dmLdn:∇n < ∇m
Δ(∇n).+1 <= Δ(∇m)
by apply: delta_le.
Qed.

Lemma troot_mod_lt m n : 
   m < n = 
   ((troot m < troot n) || ((troot m == troot n) && (tmod m < tmod n))).
m, n:nat
(m < n) = (∇m < ∇n) || (∇m == ∇n) && (tmod m < tmod n)
Proof.
m, n:nat
(m < n) = (∇m < ∇n) || (∇m == ∇n) && (tmod m < tmod n)
case: (leqP (troot n) (troot m))  => [|dmGdn] /= ; last first.
m, n:nat
dmGdn:∇m < ∇n
(m < n) = true
m, n:nat
∇n <= ∇m -> (m < n) = (∇m == ∇n) && (tmod m < tmod n)
  apply/idP.
m, n:nat
dmGdn:∇m < ∇n
m < n
m, n:nat
∇n <= ∇m -> (m < n) = (∇m == ∇n) && (tmod m < tmod n)
  apply: (leq_trans (delta_root_gt _)).
m, n:nat
dmGdn:∇m < ∇n
Δ(∇m).+1 <= n
m, n:nat
∇n <= ∇m -> (m < n) = (∇m == ∇n) && (tmod m < tmod n)
  apply: (leq_trans (delta_le dmGdn)).
m, n:nat
dmGdn:∇m < ∇n
Δ(∇n) <= n
m, n:nat
∇n <= ∇m -> (m < n) = (∇m == ∇n) && (tmod m < tmod n)
  by apply: delta_root_le.
m, n:nat
∇n <= ∇m -> (m < n) = (∇m == ∇n) && (tmod m < tmod n)
rewrite leq_eqVlt => /orP[/eqP dnEdm|dmLdn].
m, n:nat
dnEdm:∇n = ∇m
(m < n) = (∇m == ∇n) && (tmod m < tmod n)
m, n:nat
dmLdn:∇n < ∇m
(m < n) = (∇m == ∇n) && (tmod m < tmod n)
  rewrite dnEdm eqxx /=.
m, n:nat
dnEdm:∇n = ∇m
(m < n) = (tmod m < tmod n)
m, n:nat
dmLdn:∇n < ∇m
(m < n) = (∇m == ∇n) && (tmod m < tmod n)
  by rewrite {1}[m]tmodE {1}[n]tmodE dnEdm ltn_add2l.
m, n:nat
dmLdn:∇n < ∇m
(m < n) = (∇m == ∇n) && (tmod m < tmod n)
rewrite (gtn_eqF dmLdn) /=.
m, n:nat
dmLdn:∇n < ∇m
(m < n) = false
apply/idP/negP.
m, n:nat
dmLdn:∇n < ∇m
~~ (m < n)
rewrite -ltnNge ltnS ltnW //.
m, n:nat
dmLdn:∇n < ∇m
n < m
apply: (leq_trans (delta_root_gt _)).
m, n:nat
dmLdn:∇n < ∇m
Δ(∇n).+1 <= m
apply: (leq_trans _ (delta_root_le _)).
m, n:nat
dmLdn:∇n < ∇m
Δ(∇n).+1 <= Δ(∇m)
by apply: delta_le.
Qed.

(******************************************************************************)
(*                                                                            *)
(*                  Correspondence between N and N x N                        *)
(*                                                                            *)
(******************************************************************************)

(* An explicit definition of N <-> N * N *)
Definition tpair n := (troot n - tmod n, tmod n).
 
Compute zip (iota 0 20) (map tpair (iota 0 20)).
= [:: (0, (0, 0)); (1, (1, 0)); (2, (0, 1));
      (3, (2, 0)); (4, (1, 1)); (5, (0, 2));
      (6, (3, 0)); (7, (2, 1)); (8, (1, 2));
      (9, (0, 3)); (10, (4, 0)); (11, (3, 1));
      (12, (2, 2)); (13, (1, 3)); (14, (0, 4));
      (15, (5, 0)); (16, (4, 1)); (17, (3, 2));
      (18, (2, 3)); (19, (1, 4))]
: seq (nat * (nat * nat))

Definition pairt p := delta (p.1 + p.2) + p.2.

Lemma tpairt n : pairt (tpair n) = n.
n:nat
pairt (tpair n) = n
Proof.
n:nat
pairt (tpair n) = n
rewrite /tpair /pairt /= (subnK (tmod_le _)).
n:nat
Δ(∇n) + tmod n = n
by rewrite /tmod addnC subnK // delta_root_le.
Qed.

Lemma tpairt_inv p : tpair (pairt p) = p.
p:(nat * nat)%type
tpair (pairt p) = p
Proof.
p:(nat * nat)%type
tpair (pairt p) = p
case: p => a b.
a, b:nat
tpair (pairt (a, b)) = (a, b)
rewrite /tpair /pairt /= /tmod.
a, b:nat
(∇(Δ(a + b) + b) - (Δ(a + b) + b - Δ(∇(Δ(a + b) + b))),
Δ(a + b) + b - Δ(∇(Δ(a + b) + b))) = (a, b)
have ->: ∇(Δ(a + b) + b)  = a + b.
a, b:nat
∇(Δ(a + b) + b) = a + b
a, b:nat
(a + b - (Δ(a + b) + b - Δ(a + b)),
Δ(a + b) + b - Δ(a + b)) = (a, b)
  apply/eqP.
a, b:nat
∇(Δ(a + b) + b) == a + b
a, b:nat
(a + b - (Δ(a + b) + b - Δ(a + b)),
Δ(a + b) + b - Δ(a + b)) = (a, b)
  rewrite trootE leq_addr /= deltaS.
a, b:nat
Δ(a + b) + b < Δ(a + b) + (a + b).+1
a, b:nat
(a + b - (Δ(a + b) + b - Δ(a + b)),
Δ(a + b) + b - Δ(a + b)) = (a, b)
  by rewrite addnS ltnS addnCA leq_addl.
a, b:nat
(a + b - (Δ(a + b) + b - Δ(a + b)),
Δ(a + b) + b - Δ(a + b)) = (a, b)
by rewrite [delta _ + _]addnC !addnK.
Qed.