le_iff_negativeFlag_sub_eq_false
plain-language theorem explainer
On signed orbits, a ≤ b if and only if the difference b − a fails the strict-negativity flag. Order theorists and anyone wiring the integer-order certificate cite this as the flag form of non-strict comparison. The proof is a one-line symmetry of the swapped-argument lemma.
Claim. For signed orbits $a,b$ (each a pair of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), one has $a \le b$ if and only if the strict-negativity flag of $b-a$ equals $\mathsf{false}$.
background
Signed orbits are the internal integer model in the primitive recognition calculus: a structure SignedOrbit with fields pos and neg of type distinction-natural, intended as the difference $\mathrm{pos}-\mathrm{neg}$. The non-strict order is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative.
The Boolean negativeFlag is the structural dual of the nonnegative flag: it is true exactly when nonnegativity fails. Upstream, the swapped form already equates failure of negativity on $a-b$ with $b \le a$, via rewriting through the nonnegativity-flag equivalence and the nonnegativity-of-difference characterization of $\le$. The LogicNat order $\exists k,, n+k=m$ is the underlying nonnegative arithmetic, lifted here to signed differences.
proof idea
One-line term wrapper. Instantiate the upstream lemma negativeFlag_sub_eq_false_iff_le at the swapped pair $(b,a)$, which yields
$(b-a).\mathrm{negativeFlag}=\mathsf{false}\leftrightarrow a\le b$,
then take propositional symmetry (.symm) to flip the biconditional into the stated orientation $a\le b\leftrightarrow(b-a).\mathrm{negativeFlag}=\mathsf{false}$.
why it matters
Feeds the parent integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and both the Prop-level and flag-level nonnegativity characterizations; this biconditional is the flag-facing form of $\le$ dual to the nonnegativity displays.
In the foundation layer it keeps comparison decidable at the Boolean-flag surface without leaving the signed-orbit model, so later forcing and arithmetic constructions can treat integer order as a closed, certificate-backed interface rather than an open Prop-only relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.