Commit 2024-06-12 08:11 5e9f7332

feat(Algebra): auxiliary results for proofs about elliptic divisibility sequences (#13153) 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.