| Version 6 (modified by diatchki, 3 years ago) |
|---|
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 -- 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 / 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
