Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption

Following split_and, the new tactics are split_or H, split_or? H and split_or! H. The name H is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).

I was pondering whether the tactic should be split_or H or split_or in H. The second one follows the usual pattern of in+assumption, but at the same time there is not going to be a split_or tactic that works on the goal, so...