right_not_crossEq_zero_of_mul_not_crossEq_zero
plain-language theorem explainer
If the product of two ratio orbits is not cross-equivalent to zero, the right factor is not cross-equivalent to zero. Order and field-structure lemmas on the PRC integer/rational surface cite this cancellation-style fact. The proof is a one-line projection of the right conjunct from the two-sided product-nonzero characterization.
Claim. For ratio orbits $a$ and $b$, if $a\cdot b$ is not cross-equivalent to zero, then $b$ is not cross-equivalent to zero.
background
A ratio orbit (K4.7) is the internal PRC display of a rational: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence (K4.10) is the native equality relation on these displays: two ratio orbits match when the cross-scaled numerators balance as signed orbits. Multiplication and a distinguished zero orbit are defined on the same surface.
The ambient IntegerOrder module builds comparison and sign structure entirely on $\delta$-orbit positions. Upstream, the biconditional mul_not_crossEq_zero_iff records the zero-product law: the product fails to be cross-equivalent to zero if and only if both factors do. The present lemma is the right-hand projection of that law.
proof idea
One-line term proof. Apply the forward direction of the upstream biconditional (product not cross-equivalent to zero iff both factors are not) to the hypothesis, then project the second conjunct of the resulting conjunction.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed (truncated subtraction, leq display, abs-diff, and nonneg flag displays). Right-factor nonzero cancellation is a routine ingredient when that certificate reasons about nonzero denominators and signed comparisons under multiplication. The lemma lives in the Primitive Recognition Calculus foundation layer that underwrites later forcing-chain structure; it is pure rational-orbit algebra, not a T5–T8 step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.