Cross-multiplied addition, product and negation preserve RatEq; every constructed denominator is positive.
Method: native-ring. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.