Commit 2022-01-27 23:05 79e6cb09

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.