feat: port algebra/stepindex.v

[alvinylt]

Description

Port algebra/stepindex.v. It will be nice to have this ready before moving onto algebra/stepindex_finite.v as the latter requires refactoring a large number of files.

Addresses #203.

The current implementation defines SIdx as a type class that extends LT, LE and Zero from Init.Prelude so that we can reuse the notations <, ≤ and 0. Meanwhile, succᵢ is a notation defined on our own.

Checklist of definitions and theorems

• SIdx.case
• SIdx.eq_dec
• SIdx.inhabited
• SIdx.le_0_l
• SIdx.le_0_r
• SIdx.le_dec
• SIdx.le_gt_cases
• SIdx.le_lt_trans
• SIdx.le_lteq (ignored)
• SIdx.le_neq
• SIdx.le_ngt
• SIdx.le_po
• SIdx.le_succ_diag_r
• SIdx.le_succ_l
• SIdx.le_succ_l_2 (ignored)
• SIdx.le_total
• SIdx.limit
• SIdx.limit_0
• SIdx.limit_S
• SIdx.limit_finite
• SIdx.limit_lt_0
• SIdx.lt_dec
• SIdx.lt_ge_cases
• SIdx.lt_le_incl
• SIdx.lt_le_trans
• SIdx.lt_nge
• SIdx.lt_strict
• SIdx.lt_succ_diag_r (ignored)
• SIdx.lt_succ_diag_r'
• SIdx.lt_succ_r
• SIdx.lt_trans (ignored)
• SIdx.lt_trichotomy (ignored)
• SIdx.lt_wf (ignored)
• SIdx.neq_0_lt_0
• SIdx.neq_succ_0
• SIdx.nlt_0_r (ignored)
• SIdx.nlt_succ_r
• SIdx.rec
• SIdx.rec_lim
• SIdx.rec_lim_ext (ignored)
• SIdx.rec_succ
• SIdx.rec_unfold
• SIdx.rec_zero
• SIdx.succ_inj
• SIdx.succ_le_mono
• SIdx.succ_lt_mono
• SIdx.succ_neq
• SIdx.weak_case (ignored)
• SIdxFinite
• SIdxMixin
• sidx

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[Kaptch]

May I please ask to add in IrisMath instances of SIdx for ordinal type and some initial ordinal (\omega_1 would work)? Most probably non-\omega instances for SIdx would be defined on top of Mathlib, and it would be nice to have examples.