feat(order/cover): define `wcovby` (#13424)
* This defines the reflexive closure of `covby`, which I call `wcovby` ("weakly covered by")
* This is useful, since some results about `covby` still hold for `wcovby`.
* Use `wcovby` in the proofs of the properties for `covby`.
* Also define `wcovby_insert` (the motivating example, since I really want `(wcovby_insert _ _).eq_or_eq`)
