(******************************************************************************)
(*                                                                            *)
(*                              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.
2 by case: m. Qed.

Lemma prednDr m n : 0 < n -> (m + n).-1 = m + n.-1.
4
0 < n -> (m + n).-1 = m + n.-1
Proof.
9 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.
e
have [aLb|bLa] := leqP b a; last first.
11
bLa:a < b
12
11
aLb:b <= a
12
  rewrite (_ : a - _ = 0) ?sub0n //.
17
a - b = 0
19
  by apply/eqP; rewrite subn_eq0 ltnW.
1b
12
have [cLb|bLc] := leqP c b; last first.
111c
bLc:b < c
12
111c
cLb:c <= b
12
  by rewrite subnBA ?subnK // ltnW.
2b
12
rewrite (_ : c - _ = 0); last by apply/eqP; rewrite subn_eq0.
2b
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.
35
rewrite leq_subLR addnC -addnA.
37
a <= a - b + (b - c + c)
have [/subnK->|H] := leqP c b.
37
a <= a - b + b
38
H:b < c
3e
  have [/subnK->//|H] := leqP b a.
38
H:a < b
42
43
  apply: leq_trans (ltnW H) _.
4a
b <= a - b + b
43
  by apply: leq_addl.
45
3e
have := ltnW H.
45
b <= c -> a <= a - b + (b - c + c)
rewrite -subn_eq0 => /eqP->.
45
a <= a - b + (0 + c)
rewrite addnC -leq_subLR.
45
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.
61
rewrite /delta -addn2 mulnDl mulnC halfD.
63
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.
63
(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.
63
0 < n -> 0 < Δn
Proof.
70 by case: n => // n _; rewrite deltaS addnS ltnS leq_addr. Qed.

Lemma deltaE n : delta n = \sum_(i < n.+1) i.
63
Δn = \sum_(i < n.+1) i
Proof.
75
elim: n => [|n IH]; first by rewrite big_ord_recl big_ord0.
64
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.
4
m <= n -> Δm <= Δn
Proof.
81 by move=> H; apply/half_leq/leq_mul. Qed.

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

Lemma geq_deltann n : n <= delta n.
63
n <= Δn
Proof.
ad
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.
63
0 < n -> 0 < ∇n
Proof.
b3 by case: n. Qed.

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

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

(* Galois connection *)
Lemma root_delta_le m n : (n <= troot m) = (delta n <= m).
4
(n <= ∇m) = (Δn <= m)
Proof.
11b
case: leqP => [/delta_le/leq_trans->//|dmLn].
4
bc
5
dmLn:∇m < n
false = (Δn <= m)
  apply: delta_root_le.
124
126
apply/sym_equal/idP/negP.
124
~~ (Δn <= m)
rewrite -ltnNge.
124
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).
4
(∇m < n) = (m < Δn)
Proof.
133 by rewrite ltnNge root_delta_le -ltnNge. Qed.

Lemma troot_le m n : m <= n -> troot m <= troot n.
4
m <= n -> ∇m <= ∇n
Proof.
138
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).
bb
n:nat_eqType
(∇m == n) = (Δn <= m < Δn.+1)
Proof.
13d
rewrite ltnNge -!root_delta_le -ltnNge.
13f
(∇m == n) = (n <= ∇m < n.+1)
by rewrite ltnS -eqn_leq.
Qed.

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

Lemma leq_rootnn n : troot n <= n.
63
∇n <= n
Proof.
14d
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.
63
tmod (Δn) = 0
Proof.
152 by rewrite /tmod troot_delta subnn. Qed.

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

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


Lemma ltn_root m n : troot m < troot n -> m < n.
4
∇m < ∇n -> m < n
Proof.
161
rewrite root_delta_le deltaS => /(leq_trans _) -> //.
4
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).
4
∇m = ∇n -> (tmod m <= tmod n) = (m <= n)
Proof.
16a
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).
4
∇m = ∇n -> (tmod m < tmod n) = (m < n)
Proof.
16f
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].
ba
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m]
Proof.
174
have := troot_le (leqnSn m).
ba
∇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].
bb
He:∇m = ∇m.+1
176
bb
He:∇m < ∇m.+1
176
  by rewrite /tmod -He subSn ?eqxx // {2}[m]tmodE leq_addr.
183
176
rewrite orbC.
183
[&& ∇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.
183
∇m.+1 == (∇m).+1
183
∇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.
183
Δ(∇m.+1) <= m.+1
183
true && (m.+1 < Δ(∇m).+2)
191
    by rewrite {2}[m.+1]tmodE leq_addr.
183
199
190
  rewrite !deltaS {1}[m]tmodE -addnS -addnS -addnA.
183
true &&
(Δ(∇m) + (tmod m).+2 <= Δ(∇m) + ((∇m).+1 + (∇m).+2))
190
  by rewrite leq_add2l (leq_trans _ (leq_addl _ _)) // !ltnS tmod_le.
183
192
move/eqP=> He1.
bb184
He1:∇m.+1 = (∇m).+1
18b
rewrite He1 eqxx.
1a7
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
have := eqxx m.+1.
1a7
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.
1a7
Δ(∇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.
bb1841a8
He2:tmod m = ∇m + tmod m.+1
1ac
have := tmod_le m.
1b8
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.
1b8
tmod m < ∇m ->
[&& true, tmod m.+1 == 0 & tmod m == ∇m]
|| ((∇m).+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
bb1841a81b9
He3:tmod m = ∇m
1ac
  by rewrite He2 ltnNge leq_addr.
1c4
1ac
rewrite He3 -(eqn_add2l (tmod m)) {1}He3 -He2 addn0.
1c4
[&& 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))).
4
(m <= n) =
(∇m < ∇n) || (∇m == ∇n) && (tmod m <= tmod n)
Proof.
1ce
case: leqP => [|dmGdn] /= ; last first.
5
dmGdn:∇m < ∇n
(m <= n) = true
4
∇n <= ∇m ->
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
  apply/idP.
1d5
m <= n
1d8
  apply: (leq_trans (_ : _ <= delta (troot m).+1)).
1d5
m <= Δ(∇m).+1
1d5
Δ(∇m).+1 <= n
1d9
    by rewrite ltnW // delta_root_gt.
1d5
1e5
1d8
  apply: (leq_trans (_ : _ <= delta (troot n))).
1d5
Δ(∇m).+1 <= Δ(∇n)
1d5
Δ(∇n) <= n
1d9
    by apply: delta_le.
1d5
1ef
1d8
  by apply: delta_root_le.
4
1da
rewrite leq_eqVlt => /orP[/eqP dnEdm|dmLdn].
5
dnEdm:∇n = ∇m
(m <= n) = (∇m == ∇n) && (tmod m <= tmod n)
5
dmLdn:∇n < ∇m
1fb
  rewrite dnEdm eqxx /=.
1f9
(m <= n) = (tmod m <= tmod n)
1fc
  by rewrite {1}[m]tmodE {1}[n]tmodE dnEdm leq_add2l.
1fe
1fb
rewrite (gtn_eqF dmLdn) /=.
1fe
(m <= n) = false
apply/idP/negP.
1fe
~~ (m <= n)
rewrite -ltnNge.
1fe
n < m
apply: (leq_trans (delta_root_gt _)).
1fe
Δ(∇n).+1 <= m
apply: (leq_trans _ (delta_root_le _)).
1fe
Δ(∇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))).
4
(m < n) = (∇m < ∇n) || (∇m == ∇n) && (tmod m < tmod n)
Proof.
21c
case: (leqP (troot n) (troot m))  => [|dmGdn] /= ; last first.
1d5
(m < n) = true
4
∇n <= ∇m -> (m < n) = (∇m == ∇n) && (tmod m < tmod n)
  apply/idP.
1d5
m < n
224
  apply: (leq_trans (delta_root_gt _)).
1e8224
  apply: (leq_trans (delta_le dmGdn)).
1f2224
  by apply: delta_root_le.
4
226
rewrite leq_eqVlt => /orP[/eqP dnEdm|dmLdn].
1f9
(m < n) = (∇m == ∇n) && (tmod m < tmod n)
1fe
235
  rewrite dnEdm eqxx /=.
1f9
(m < n) = (tmod m < tmod n)
236
  by rewrite {1}[m]tmodE {1}[n]tmodE dnEdm ltn_add2l.
1fe
235
rewrite (gtn_eqF dmLdn) /=.
1fe
(m < n) = false
apply/idP/negP.
1fe
~~ (m < n)
rewrite -ltnNge ltnS ltnW //.
210
apply: (leq_trans (delta_root_gt _)).213
apply: (leq_trans _ (delta_root_le _)).217
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.
63
pairt (tpair n) = n
Proof.
24a
rewrite /tpair /pairt /= (subnK (tmod_le _)).
63
Δ(∇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.
253
case: p => a b.
a, b:nat
tpair (pairt (a, b)) = (a, b)
rewrite /tpair /pairt /= /tmod.
25c
(∇(Δ(a + b) + b) - (Δ(a + b) + b - Δ(∇(Δ(a + b) + b))),
Δ(a + b) + b - Δ(∇(Δ(a + b) + b))) = (a, b)
have ->: ∇(Δ(a + b) + b)  = a + b.
25c
∇(Δ(a + b) + b) = a + b
25c
(a + b - (Δ(a + b) + b - Δ(a + b)),
Δ(a + b) + b - Δ(a + b)) = (a, b)
  apply/eqP.
25c
∇(Δ(a + b) + b) == a + b
267
  rewrite trootE leq_addr /= deltaS.
25c
Δ(a + b) + b < Δ(a + b) + (a + b).+1
267
  by rewrite addnS ltnS addnCA leq_addl.
25c
269
by rewrite [delta _ + _]addnC !addnK.
Qed.