wiki:TypeNats/Interact2

Version 3 (modified by diatchki, 3 years ago) (diff)

--

a + b ~ c
  a + b ~ d <=> c ~ d
  b + a ~ d <=> c ~ d

  a + d ~ c <=> b ~ d
  d + a ~ c <=> b ~ d
  d + b ~ c <=> a ~ d
  b + d ~ c <=> a ~ d

m + b ~ c
  n + d ~ c <=> {m - n} + b ~ d  -- n <= m
  n + d ~ c <=> {n - m} + d ~ b  -- m >=m
a * b ~ c
  a * b ~ d <=> c ~ d
  b * a ~ d <=> c ~ d

m * b ~ c
  n * b ~ c <=> (b ~ 0, c ~ 0)    -- m /= n
  n * d ~ c <=> {m / g} * b ~ {n / g} * d    -- g = gcd m n, g /= 1, replaces both assumptions