Try to define `ConvexSpace` without strict order

[ooovi]

mathlib defintion wants StrictOrderedRing but OrderedRing is probably sufficient. we should PR that because like this a lot of our theory gets less general.