Order isomorphism along homogenization

[martinwintermath]

ConvexSet simeq_o {C : PointedCone | C \le weight.positive_+}

[ooovi]

this would help with e.g. showing that the intersection of two homogenization cones is a homogenization cone. useful for

protected theorem inter (hP₁ : IsPolytope R P₁) (hP₂ : IsPolytope R P₂) :
    IsPolytope R (P₁ ∩ P₂) := by

[ooovi]

this wuold also help proving homogenize_isFaceOf without pain maybe