Delightful typo in a nontrivial routine

Stream: lean4

[Geoffrey Irving]

Here's a case-analysis intensive routine from what I'm currently working on, which is a fun example of programming alongside theorem proving:

/-- Multiply, changing `s` -/
def Interval.mul (x : Interval s) (y : Interval t) (u : Int64) : Interval u :=
  bif x == 0 || y == 0 then 0
  else bif x.lo == nan || x.hi == nan || y.lo == nan || y.hi == nan then ⟨nan,nan⟩
  else bif x.lo.n.isNeg != x.hi.n.isNeg && y.lo.n.isNeg != x.hi.n.isNeg then  -- x,y have mixed sign
    ⟨min (x.lo.mul y.hi u false) (x.hi.mul y.lo u false),
     max (x.lo.mul y.lo u true) (x.hi.mul y.hi u true)⟩
  else -- At least one of x,y has constant sign, so we can save multiplications
    let (a,b,c,d) := match (x.lo.n.isNeg, x.hi.n.isNeg, y.lo.n.isNeg, y.hi.n.isNeg) with
      | (false, _, false, _)    => (x.lo, x.hi, y.lo, y.hi)  -- 0 ≤ x, 0 ≤ y
      | (false, _, true, false) => (x.hi, x.hi, y.lo, y.hi)  -- 0 ≤ x, 0 ∈ y
      | (false, _, _, true)     => (x.hi, x.lo, y.lo, y.hi)  -- 0 ≤ x, y ≤ 0
      | (true, false, false, _) => (x.lo, x.hi, y.hi, y.hi)  -- 0 ∈ x, 0 ≤ y
      | (true, false, _, _)     => (x.hi, x.lo, y.lo, y.lo)  -- 0 ∈ x, y ≤ 0 (0 ∈ y is impossible)
      | (_, true, false, _)     => (x.lo, x.hi, y.hi, y.lo)  -- x ≤ 0, 0 ≤ y
      | (_, true, true, false)  => (x.lo, x.lo, y.hi, y.lo)  -- x ≤ 0, 0 ∈ y
      | (_, true, _, true)      => (x.hi, x.lo, y.hi, y.lo)  -- x ≤ 0, y ≤ 0
    ⟨a.mul c u false, b.mul d u true⟩

I proved this code correct: it is a conservative approximation of real multiplication. However, it also has a typo: the first line in the following should be the second:

  else bif x.lo.n.isNeg != x.hi.n.isNeg && y.lo.n.isNeg != x.hi.n.isNeg then  -- wrong: last x should be a y
  else bif x.lo.n.isNeg != x.hi.n.isNeg && y.lo.n.isNeg != y.hi.n.isNeg then  -- correct

But it doesn't matter! The two comparisons y.lo.n.isNeg != x.hi.n.isNeg and y.lo.n.isNeg != y.hi.n.isNeg are equal when it matters, since if x has mixed sign then x.hi must be positive. And indeed my split-and-simplify proof didn't notice this typo, since the relevant case simplified to the same thing. :)

[Mario Carneiro]

if it's still correct, is it really a typo?