Library Numbers.nat_compl
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Additional results about natural numbers, for both the Coq standard library
and the Mathematical Components library.
All lemmas about natural numbers from the Coq standard library have names
prefixed with "nat_", except those about even and odd numbers.
This module may be used through the import of Numbers.Numbers_wDep,
Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or
Lebesgue.Bochner.Bochner_wDep, where it is exported.
Brief description
Description
- nat_ind2× provide several induction schemes in N², including a strong induction scheme with nat_ind2_strong;
- nat_has_unique_least_element is a specialization of Coq.Arith.Wf_nat.dec_inh_nat_subset_has_unique_least_element with less hypotheses;
- nat_has_unique_greatest_element is the counterpart for subsets of N that are bounded from above.
Usage
From Requisite Require Import stdlib ssr_wMC.
From Logic Require Import logic_compl.
Local Open Scope nat_scope.
Section nat_compl.
Lemma inhabited_nat : inhabited nat.
Proof. apply (inhabits 0). Qed.
Lemma nat_plus_0_l : ∀ {n1 n2}, n1 = 0 → n1 + n2 = n2.
Proof. intros; subst; apply add0n. Qed.
Lemma nat_plus_0_r : ∀ {n1 n2}, n2 = 0 → n1 + n2 = n1.
Proof. intros; subst; apply addn0. Qed.
Lemma nat_plus_minus_l :
∀ {n1 n2}, (n1 ≤ n2)%coq_nat → (n2 - n1) + n1 = n2.
Proof. intros; rewrite addnC; auto with arith. Qed.
Lemma nat_plus_minus_r :
∀ {n1 n2}, (n1 ≤ n2)%coq_nat → n1 + (n2 - n1) = n2.
Proof. auto with arith. Qed.
Lemma Even_0 : Nat.Even 0.
Proof. exact Nat.Private_Parity.Even_0. Qed.
Lemma Even_1 : ¬ Nat.Even 1.
Proof. exact Nat.Private_Parity.Even_1. Qed.
Lemma Even_SS : ∀ n, Nat.Even n ↔ Nat.Even n.+2.
Proof. exact Nat.Private_Parity.Even_2. Qed.
Lemma Even_2 : Nat.Even 2.
Proof. rewrite -Even_SS; apply Even_0. Qed.
Lemma Even_3 : ¬ Nat.Even 3.
Proof. rewrite -Even_SS; apply Even_1. Qed.
Lemma Odd_0 : ¬ Nat.Odd 0.
Proof. exact Nat.Private_Parity.Odd_0. Qed.
Lemma Odd_1 : Nat.Odd 1.
Proof. exact Nat.Private_Parity.Odd_1. Qed.
Lemma Odd_SS : ∀ n, Nat.Odd n ↔ Nat.Odd n.+2.
Proof. exact Nat.Private_Parity.Odd_2. Qed.
Lemma Odd_2 : ¬ Nat.Odd 2.
Proof. rewrite -Odd_SS; apply Odd_0. Qed.
Lemma Odd_3 : Nat.Odd 3.
Proof. rewrite -Odd_SS; apply Odd_1. Qed.
Lemma nat_ind2 :
∀ (P : nat → nat → Prop),
P 0 0 →
(∀ m n, P m n → P m.+1 n) →
(∀ m n, P m n → P m n.+1) →
∀ m n, P m n.
Proof. intros P H00 HSn HmS; induction m; induction n; auto. Qed.
Lemma nat_ind2_11 :
∀ (P : nat → nat → Prop),
P 1 1 →
(∀ m n, m ≠ 0 → n ≠ 0 → P m n → P m.+1 n) →
(∀ m n, m ≠ 0 → n ≠ 0 → P m n → P m n.+1) →
∀ m n, m ≠ 0 → n ≠ 0 → P m n.
Proof.
intros P Hm1 H1n H m n; destruct m, n; [easy.. |]; intros _ _.
apply (nat_ind2 (fun m n ⇒ P m.+1 n.+1)); auto.
Qed.
Lemma nat_ind2_alt_1l :
∀ (P : nat → nat → Prop),
(∀ m, m ≠ 0 → P m 0) → (∀ n, P 1 n) →
(∀ m n, m ≠ 0 → P m.+1 n → P m n.+1 → P m.+1 n.+1) →
∀ m n, m ≠ 0 → P m n.
Proof.
intros P Hm0 H1n H m; destruct m; try easy; induction m; [| induction n]; auto.
Qed.
Lemma nat_ind2_alt_1r :
∀ (P : nat → nat → Prop),
(∀ m, P m 1) → (∀ n, n ≠ 0 → P 0 n) →
(∀ m n, n ≠ 0 → P m.+1 n → P m n.+1 → P m.+1 n.+1) →
∀ m n, n ≠ 0 → P m n.
Proof.
intros P Hm1 H0n H; induction m;
[| intros n; destruct n; [easy.. | induction n]]; auto.
Qed.
Lemma nat_ind2_alt_00 :
∀ (P : nat → nat → Prop),
(∀ m, m ≠ 0 → P m 0) → (∀ n, n ≠ 0 → P 0 n) →
(∀ m n, P m.+1 n → P m n.+1 → P m.+1 n.+1) →
∀ m n, (m ≠ 0 ∨ n ≠ 0) → P m n.
Proof.
intros P Hm0 H0n H m n [H0 | H0].
apply nat_ind2_alt_1l; auto; intros n'; induction n'; auto.
apply nat_ind2_alt_1r; auto; intros m'; induction m'; auto.
Qed.
Lemma nat_ind2_alt :
∀ (P : nat → nat → Prop),
(∀ m, P m 0) → (∀ n, P 0 n) →
(∀ m n, P m.+1 n → P m n.+1 → P m.+1 n.+1) →
∀ m n, P m n.
Proof. intros P Hm0 H0n H m n; destruct m, n; [..| apply nat_ind2_alt_00]; auto.
Qed.
Lemma nat_ind2_alt_11 :
∀ (P : nat → nat → Prop),
(∀ m, (0 < m)%coq_nat → P m 1) → (∀ n, (0 < n)%coq_nat → P 1 n) →
(∀ m n, (0 < m)%coq_nat → (0 < n)%coq_nat →
P m.+1 n → P m n.+1 → P m.+1 n.+1) →
∀ m n, (0 < m)%coq_nat → (0 < n)%coq_nat → P m n.
Proof.
intros P Hm1 H1n H m n; destruct m, n; [easy.. | intros _ _].
apply (nat_ind2_alt (fun m n ⇒ P m.+1 n.+1)); clear m n.
intros m; apply Hm1, Nat.neq_0_lt_0; easy.
intros n; apply H1n, Nat.neq_0_lt_0; easy.
intros m n; apply H; apply Nat.neq_0_lt_0; easy.
Qed.
Lemma nat_ind_strong :
∀ (P : nat → Prop),
(∀ n, (∀ k, (k < n)%coq_nat → P k) → P n) →
∀ n, P n.
Proof. intros; apply lt_wf_ind; easy. Qed.
Lemma nat_ind2_strong :
∀ (P : nat → nat → Prop),
(∀ m n, (∀ m1 n1, (m1 ≤ m)%coq_nat → (n1 ≤ n)%coq_nat →
(m1, n1) ≠ (m, n) → P m1 n1) → P m n) →
∀ m n, P m n.
Proof.
intros P HP; apply (nat_ind_strong (fun m ⇒ ∀ n, P m n)); intros m Hm.
apply nat_ind_strong; intros n Hn.
apply HP; move⇒ m1 n1 /Nat.le_lteq Hm1 /Nat.le_lteq Hn1 H1.
destruct Hm1; [apply Hm; easy |]; subst.
destruct Hn1; [apply Hn; easy |]; subst.
contradict H1; easy.
Qed.
Lemma lt_1 : ∀ {n}, (n < 1)%coq_nat ↔ n = 0.
Proof. lia. Qed.
Lemma lt_2 : ∀ {n}, (n < 2)%coq_nat ↔ n = 0 ∨ n = 1.
Proof. lia. Qed.
Lemma lt_S :
∀ {N n}, (n < N.+1)%coq_nat ↔ (n < N)%coq_nat ∨ n = N.
Proof. lia. Qed.
Lemma nat_le_antisym_rev :
∀ {m n}, m = n → (m ≤ n)%coq_nat ∧ (n ≤ m)%coq_nat.
Proof. intros; subst; split; apply Nat.le_refl. Qed.
Lemma nat_le_antisym_equiv :
∀ {m n}, m = n ↔ (m ≤ n)%coq_nat ∧ (n ≤ m)%coq_nat.
Proof.
intros; split; [apply nat_le_antisym_rev |].
intros [H1 H2]; apply Nat.le_antisymm; easy.
Qed.
Lemma nat_le_total : ∀ m n, (m ≤ n)%coq_nat ∨ (n ≤ m)%coq_nat.
Proof. exact Nat.le_ge_cases. Qed.
Lemma nat_lt_total_strict :
∀ m n, m ≠ n → (m < n)%coq_nat ∨ (n < m)%coq_nat.
Proof. apply Nat.lt_gt_cases. Qed.
Lemma nat_neq_0_equiv : ∀ n, n ≠ 0 ↔ (0 < n)%coq_nat.
Proof. lia. Qed.
Lemma nat_eq_le : ∀ m n, m = n → (m ≤ n)%coq_nat.
Proof. lia. Qed.
Lemma nat_leS : ∀ n, (n ≤ n.+1)%coq_nat.
Proof. exact Nat.le_succ_diag_r. Qed.
Lemma nat_ltS : ∀ n, (n < n.+1)%coq_nat.
Proof. exact Nat.lt_succ_diag_r. Qed.
Lemma nat_le_ltS : ∀ {n i}, (i ≤ n)%coq_nat → (i < n.+1)%coq_nat.
Proof. lia. Qed.
Lemma nat_pred_to_succ : ∀ m n, m ≠ 0 → m.-1 = n → m = n.+1.
Proof. lia. Qed.
Lemma nat_succ_to_pred : ∀ m n, m = n.+1 → m.-1 = n.
Proof. lia. Qed.
Lemma nat_plus_reg_l :
∀ n n1 n2, (n + n1)%coq_nat = (n + n2)%coq_nat → n1 = n2.
Proof. lia. Qed.
Lemma nat_plus_reg_r :
∀ n n1 n2, (n1 + n)%coq_nat = (n2 + n)%coq_nat → n1 = n2.
Proof. lia. Qed.
Lemma nat_plus_zero_reg_l : ∀ m n, (m + n)%coq_nat = m → n = 0.
Proof. lia. Qed.
Lemma nat_plus_zero_reg_r : ∀ m n, (m + n)%coq_nat = n → m = 0.
Proof. lia. Qed.
Lemma nat_plus_def : ∀ m n, (m + n)%coq_nat = 0 → m = 0 ∧ n = 0.
Proof. lia. Qed.
Lemma nat_add_2_l : ∀ n, (2 + n)%coq_nat = n.+2.
Proof. lia. Qed.
Lemma nat_add_2_r : ∀ n, (n + 2)%coq_nat = n.+2.
Proof. lia. Qed.
Lemma nat_add_sub_l :
∀ {m n p}, m = (n + p)%coq_nat → n = (m - p)%coq_nat.
Proof. lia. Qed.
Lemma nat_add_sub_equiv_l :
∀ {m n p},
(p ≤ m)%coq_nat → m = (n + p)%coq_nat ↔ n = (m - p)%coq_nat.
Proof. lia. Qed.
Lemma nat_add_sub_r :
∀ {m n p}, m = (n + p)%coq_nat → p = (m - n)%coq_nat.
Proof. lia. Qed.
Lemma nat_add_sub_equiv_r :
∀ {m n p},
(n ≤ m)%coq_nat → m = (n + p)%coq_nat ↔ p = (m - n)%coq_nat.
Proof. lia. Qed.
Lemma nat_sub2_r :
∀ m n, (n ≤ m)%coq_nat → (m - (m - n)%coq_nat)%coq_nat = n.
Proof. lia. Qed.
Lemma nat_double_S : ∀ n, (2 × n.+1)%coq_nat = (2 × n)%coq_nat.+2.
Proof. intros; rewrite Nat.mul_succ_r; apply nat_add_2_r. Qed.
Lemma nat_S_double_S :
∀ n, ((2 × (n.+1))%coq_nat + 1)%coq_nat = (2 × n)%coq_nat.+3.
Proof. intros; rewrite nat_double_S Nat.add_1_r; easy. Qed.
Lemma nat_le_S_neq :
∀ {m n}, (m ≤ n.+1)%coq_nat → m ≠ n.+1 → (m ≤ n)%coq_nat.
Proof. lia. Qed.
Lemma nat_le_S_lt :
∀ {m n}, (m ≤ n.+1)%coq_nat → (n < m)%coq_nat → m = n.+1.
Proof. lia. Qed.
Lemma nat_lt_lt_S :
∀ m n p, (m < n)%coq_nat → (n < p.+1)%coq_nat → (m < p)%coq_nat.
Proof. lia. Qed.
Lemma nat_lt2_add_lt1_sub_l :
∀ m n p, (n ≤ m)%coq_nat →
(m < (n + p)%coq_nat)%coq_nat ↔ ((m - n)%coq_nat < p)%coq_nat.
Proof. lia. Qed.
Lemma nat_lt2_add_lt1_sub_r :
∀ m n p, (p ≤ m)%coq_nat →
(m < (n + p)%coq_nat)%coq_nat ↔ ((m - p)%coq_nat < n)%coq_nat.
Proof. lia. Qed.
Lemma nat_lt2_sub_lt1_add_l :
∀ m n p, (m < (n - p)%coq_nat)%coq_nat ↔ ((m + p)%coq_nat < n)%coq_nat.
Proof. lia. Qed.
Lemma nat_lt2_sub_lt1_add_r :
∀ m n p, (p < (n - m)%coq_nat)%coq_nat ↔ ((m + p)%coq_nat < n)%coq_nat.
Proof. lia. Qed.
Lemma nat_sub_le_mono_r :
∀ m n p,
(p ≤ m)%coq_nat → (p ≤ n)%coq_nat →
((m - p)%coq_nat ≤ (n - p)%coq_nat)%coq_nat → (m ≤ n)%coq_nat.
Proof. lia. Qed.
Lemma nat_sub_lt_mono_r :
∀ m n p,
(p ≤ m)%coq_nat → (p ≤ n)%coq_nat →
((m - p)%coq_nat < (n - p)%coq_nat)%coq_nat → (m < n)%coq_nat.
Proof. lia. Qed.
Lemma nat_has_unique_least_element :
∀ (P : nat → Prop) n1,
P n1 → ∃! n0, P n0 ∧ ∀ n, P n → (n0 ≤ n)%coq_nat.
Proof.
intros P n1 H1; destruct (dec_inh_nat_subset_has_unique_least_element P)
as [n0 Hn0]; [intros; apply classic | ∃ n1; easy |]; ∃ n0; easy.
Qed.
Lemma nat_has_least_element :
∀ (P : nat → Prop) n1,
P n1 → ∃ n0, P n0 ∧ ∀ n, P n → (n0 ≤ n)%coq_nat.
Proof.
intros P n1 H1; destruct (nat_has_unique_least_element P n1 H1) as [n0 Hn0];
∃ n0; apply Hn0.
Qed.
Lemma nat_has_unique_greatest_element :
∀ (P : nat → Prop) n1 n2,
P n1 → (∀ n, (n2 < n)%coq_nat → ¬ P n) →
∃! n0,
(n0 ≤ n2)%coq_nat ∧ P n0 ∧ ∀ n, P n → (n ≤ n0)%coq_nat.
Proof.
intros P n1 n2 Hn1 Hn2; pose (Q n := ∀ i, (n ≤ i)%coq_nat → ¬ P i).
destruct (nat_has_unique_least_element Q n2.+1) as [n0 [[Hn01 Hn02] Hn03]];
[intros i; apply Hn2 |].
destruct n0 as [| n0]; [contradict Hn1; apply Hn01, Nat.le_0_l |].
∃ n0; repeat split.
apply le_S_n, Hn02; easy.
destruct (classic (P n0)) as [H | H]; [easy |].
assert (Hn0 : Q n0)
by now intros i Hi; destruct (le_lt_eq_dec n0 i Hi); [apply Hn01 | subst].
specialize (Hn02 _ Hn0); contradict Hn02; lia.
intros i Hi1; destruct (le_lt_dec i n0) as [| Hi2]; [easy |].
contradict Hi1; apply (Hn01 i); easy.
intros m [Hm1 [Hm2 Hm3]]; apply Nat.succ_inj, Hn03; split.
intros i Hi1 Hi2; contradict Hi1; apply Nat.nle_gt, Nat.lt_succ_r, Hm3; easy.
intros i Hi1; specialize (Hn02 _ Hi1).
destruct (le_lt_dec i m) as [Hi2 | Hi2]; [contradict Hm2; apply Hi1 |]; easy.
Qed.
Lemma nat_has_greatest_element :
∀ (P : nat → Prop) n1 n2,
P n1 → (∀ n, (n2 < n)%coq_nat → ¬ P n) →
∃ n0,
(n0 ≤ n2)%coq_nat ∧ P n0 ∧ ∀ n, P n → (n ≤ n0)%coq_nat.
Proof.
intros P n1 n2 H1 H2; destruct (nat_has_unique_greatest_element P n1 n2 H1 H2)
as [n0 Hn0]; ∃ n0; apply Hn0.
Qed.
Lemma nat_lt_eq_gt_dec :
∀ n m, { (n < m)%coq_nat } + { n = m } + { (m < n)%coq_nat }.
Proof.
intros n m; destruct (le_lt_dec n m) as [H1 | H1].
destruct (le_lt_eq_dec _ _ H1) as [H2 | H2]; left; [left | right]; easy.
right; easy.
Qed.
Fixpoint max_n (f : nat → nat) (n : nat) : nat :=
match n with
| 0 ⇒ f 0%nat
| S n ⇒ max (f (S n)) (max_n f n)
end.
Lemma max_n_correct :
∀ (f : nat → nat) n p, (p ≤ n)%coq_nat → (f p ≤ max_n f n)%coq_nat.
Proof.
intros f n p H; induction n.
rewrite Nat.le_0_r in H; now rewrite H.
simpl; case (le_lt_eq_dec p (S n)); try easy; intros Hp.
apply Nat.le_trans with (max_n f n).
apply IHn; lia.
apply Nat.le_max_r.
rewrite Hp; apply Nat.le_max_l.
Qed.
Lemma pred_mul_S :
∀ m n, (m.+1 × n.+1)%coq_nat.-1 = ((m.+1 × n)%coq_nat + m)%coq_nat.
Proof. lia. Qed.
Lemma lt_mul_S :
∀ m n p,
(p < (m.+1 × n.+1)%coq_nat)%coq_nat ↔
(p < ((m.+1 × n.+1)%coq_nat.-1).+1)%coq_nat.
Proof. lia. Qed.
Lemma pow_pos : ∀ m n, (0 < m)%coq_nat → (0 < Nat.pow m n)%coq_nat.
Proof.
intros m n; destruct m; [easy | intros _].
destruct m; [rewrite Nat.pow_1_l; lia |].
destruct n; [rewrite Nat.pow_0_r; lia |].
apply Nat.lt_trans with n.+1; [lia |].
apply Nat.pow_gt_lin_r; lia.
Qed.
End nat_compl.
Section ssrnat_compl.
Lemma lt_ltn : ∀ {m n}, (m < n)%coq_nat → m < n.
Proof. move=>> /ltP; easy. Qed.
Lemma le_leq : ∀ {m n}, (m ≤ n)%coq_nat → m ≤ n.
Proof. move=>> /leP; easy. Qed.
Lemma ltn_asym : ∀ m n, m < n < m = false.
Proof. move=>>; rewrite !ltnNge -negb_or; apply negbF, leq_total. Qed.
Lemma ltn_2_dec : ∀ {n}, n < 2 → {n = 0} + {n = 1}.
Proof.
intros n H; induction n as [| n Hn].
left; easy.
destruct Hn as [Hn | Hn]; auto with arith.
contradict H; rewrite Hn; easy.
Qed.
Lemma leq_1_dec : ∀ {n}, n ≤ 1 → {n = 0} + {n = 1}.
Proof. intros; apply ltn_2_dec; easy. Qed.
Lemma ltn_3_dec : ∀ {n}, n < 3 → {n = 0} + {n = 1} + {n = 2}.
Proof.
intros n H; induction n as [| n Hn].
left; left; easy.
destruct Hn as [[Hn | Hn] | Hn]; auto with arith.
contradict H; rewrite Hn; easy.
Qed.
Lemma leq_2_dec : ∀ {n}, n ≤ 2 → {n = 0} + {n = 1} + {n = 2}.
Proof. intros; apply ltn_3_dec; easy. Qed.
Lemma ltnSS : ∀ {m n}, (m < n) = (m.+1 < n.+1).
Proof. intros; rewrite ltnS; easy. Qed.
Lemma ltnSSn : ∀ {n}, n < n.+2.
Proof. easy. Qed.
Lemma ltn_neq : ∀ {n i}, i < n → i ≠ n.
Proof. move=>>; rewrite contra_not_r_equiv; move⇒ ->; rewrite ltnn; easy. Qed.
Lemma leq_neq_ltn : ∀ {n i}, i ≤ n → i ≠ n → i < n.
Proof.
move=>> /leP Hi1 Hi2; apply /ltP.
destruct (le_lt_eq_dec _ _ Hi1) as [Hi3 | Hi3]; [| contradict Hi2]; easy.
Qed.
Lemma ltn_leq_neq : ∀ {n i}, i < n → i ≤ n ∧ i ≠ n.
Proof. intros; split; [apply ltnW | apply ltn_neq]; easy. Qed.
Lemma ltn_equiv : ∀ {n i}, i < n ↔ i ≤ n ∧ i ≠ n.
Proof.
intros; split; [apply ltn_leq_neq | intros; apply leq_neq_ltn; easy].
Qed.
Lemma ltnS_neq_ltn : ∀ {n i}, i < n.+1 → i ≠ n → i < n.
Proof. move=>>; rewrite ltnS; apply leq_neq_ltn. Qed.
Lemma leqS : ∀ {m n}, m ≤ n → m.+1 ≤ n.+1.
Proof. easy. Qed.
Lemma leqS_rev : ∀ {m n}, m.+1 ≤ n.+1 → m ≤ n.
Proof. easy. Qed.
Lemma leqS_equiv : ∀ {m n}, m ≤ n ↔ m.+1 ≤ n.+1.
Proof. easy. Qed.
Lemma ltn_S : ∀ j i n, i < j → j < n → i.+1 < n.
Proof. move=>> /ltP H1 /ltP H2; apply /ltP; lia. Qed.
Lemma nltn_geq : ∀ {m n}, ¬ m < n ↔ n ≤ m.
Proof. intros m n; rewrite (leqNgt n m); split; move⇒ /negP; easy. Qed.
Lemma nleq_gtn : ∀ {m n}, ¬ m ≤ n ↔ n < m.
Proof. intros m n; rewrite (ltnNge n m); split; move⇒ /negP; easy. Qed.
Lemma ltnP_gtnS : ∀ {m n}, n ≠ 0 → m < n.-1 → m.+1 < n.
Proof. move=>> Hn /ltP H; apply /ltP; lia. Qed.
Lemma subn1_lt : ∀ {n}, 0 < n → n - 1 < n.
Proof. intros; rewrite ltn_subCl; try rewrite subnn //; easy. Qed.
Lemma addn0_sym : ∀ n, n = n + 0.
Proof. intros; rewrite addn0 //. Qed.
Lemma add0n_sym : ∀ n, n = 0 + n.
Proof. easy. Qed.
Lemma addn1_sym : ∀ n, n.+1 = n + 1.
Proof. intros; rewrite addn1 //. Qed.
Lemma add1n_sym : ∀ n, n.+1 = 1 + n.
Proof. easy. Qed.
Lemma addSn_sym : ∀ m n, (m + n).+1 = m.+1 + n.
Proof. intros; apply eq_sym, addSn. Qed.
Lemma addnS_sym : ∀ m n, (m + n).+1 = m + n.+1.
Proof. intros; apply eq_sym, addnS. Qed.
Lemma addn_inj_l : ∀ p {m n}, m + p = n + p → m = n.
Proof. move=>>; rewrite -plusE; lia. Qed.
Lemma addn_inj_r : ∀ p {m n}, p + m = p + n → m = n.
Proof. move=>>; rewrite -plusE; lia. Qed.
Lemma addn1K : ∀ n, (n + 1).-1 = n.
Proof. intros; rewrite addn1 //. Qed.
Lemma addn1_pos : ∀ n, 0 < n + 1.
Proof. intros; rewrite addn1 //. Qed.
Lemma addn_is_subn : ∀ m n p, m = n + p → m - n = p.
Proof. intros; subst; apply addKn. Qed.
Lemma addn_subn : ∀ {n} i, (i < n.+1)%coq_nat → i + (n - i) = n.
Proof. intros; apply subnKC, ltnSE; apply /ltP; easy. Qed.
End ssrnat_compl.