pub fn canonicalize_comparison(e: &Spanned<Expr>) -> Spanned<Expr>Expand description
Canonicalize a when-clause comparison to a single normal direction:
rewrite a > b to b < a and a >= b to b <= a by swapping the
operands. This is a pure operand swap, NEVER a negation — a strict
bound stays strict (Gt -> Lt) and a nonstrict bound stays nonstrict
(Gte -> Lte), so it can never turn a semantically-load-bearing r < d
into r <= d. Any expression that is not a >/>= comparison
(already-canonical </<=, ==/!=, or a non-comparison predicate)
is returned unchanged, so canonical-direction clauses round-trip
byte-identically. This is a lowering-privilege normalization internal to
proof RECOGNITION only: the emitted theorem/lemma still renders the
user’s original when surface form, so nothing user-visible is flipped.