feat(Algebra): auxiliary results for proofs about elliptic divisibility sequences

[alreadydone]

trafficstars

Int.strongRec: if a proposition holds for integers less than a threshold, and it holds for an integer above the threshold if it holds for all smaller integers, then it holds for all integers.

negOnePow_abs says (-1)^|n|=(-1)^n

pos_iff_two_le_of_even and lt_iff_add_two_le_of_even_sub are two lemmas about the interaction of parity and the order on the integers.

Equiv.Perm.closure_isSwap is strengthened to say the submonoid generated by transpositions is the whole group, and moreover show transpositions of adjacent elements are enough.

---

[alreadydone]

Nice, the cache error finally goes away.

[github-actions[bot]]

PR summary 884b42d7e0

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.GroupTheory.Perm.Sign	719	605	-114 (-15.86%)
Mathlib.LinearAlgebra.Multilinear.Basic	768	674	-94 (-12.24%)

---

Declarations diff

+ add_le_iff_le_sub + add_le_zero_iff_le_neg + add_le_zero_iff_le_neg' + add_nonnneg_iff_neg_le + add_nonnneg_iff_neg_le' + add_two_le_iff_lt_of_even_sub + div_ne_zero_iff_of_dvd + inductionOn'_add_one + inductionOn'_self + inductionOn'_sub_one + le_add_iff_lt_of_dvd_sub + le_add_iff_sub_le + le_iff_ne_zero_of_dvd + le_iff_pos_of_dvd + mclosure_isSwap + mclosure_swap_castSucc_succ + negOnePow_abs + strongRec + strongRec_of_ge + strongRec_of_lt + two_le_iff_pos_of_even

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[YaelDillies]

I added the few lemmas I need for #13683 and golfed your Int analogs on the way. I was going to open another PR, but then I noticed yours was already solely prerequisite lemmas. Hope you don't mind.

[alreadydone]

Thanks, LGTM!

[YaelDillies]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style