wiki:TypeNats/Interact2
a <= b
  (b <= a) <=> a ~ b
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  -- n >= 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 / n} * b ~ d   -- n `divides` m
  n * d ~ c <=> {n / m} * d ~ b   -- m `divides` n

  b + c ~ d <=> {m + 1} * b ~ d
  c + b ~ d <=> {m + 1} * b ~ d
Last modified 3 years ago Last modified on Jan 7, 2011 2:34:30 AM