feat(algebra/order/sub/defs): make `has_ordered_sub` a Prop (#18810)
`has_ordered_sub` was incorrectly a Type, because of a Lean 3 bug. This is a backport of mathlib4 [#3436](https://github.com/leanprover-community/mathlib4/pull/3436) .
Co-authored-by: Alex J Best <alex.j.best@gmail.com>