mathlib3

79e6cb09 - feat(order/succ_pred/relation): `succ`/`pred` inductions on relations (#11518)

feat(order/succ_pred/relation): `succ`/`pred` inductions on relations (#11518) * Rename file `order.succ_pred` -> `order.succ_pred.basic` * Generalize induction principles `succ.rec` and `pred.rec`, make the argument order more "induction-like" and add the attribute `@[elab_as_eliminator]` * Proof properties about `refl_trans_gen` and `trans_gen` in a `is_succ_archimedean` order. * Proof some monotonicity properties of closure operations.