Triangle/product inequalities and inclusion-preserving addition, multiplication and reciprocal on intervals with positive lower endpoint.
Method: native-order. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.