Commit 2021-10-12 08:59 2e72f352

refactor(data/opposite): Remove the op_induction tactic (#9660) The induction tactic is already powerful enough for this; we don't have order_dual_induction or nat_induction as tactics. The bulk of this change is replacing op_induction x with induction x using opposite.rec. This leaves behind the non-interactive op_induction' which is still needed as a tidy hook. This also renames the def opposite.op_induction to opposite.rec to match order_dual.rec etc.