Further results about mod.

This file proves some results about mod that are useful for bitblasting, in particular Nat.mod_mul : x % (a * b) = x % a + a * (x / a % b) and its corollary Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b).

It contains the necessary preliminary results relating order and * and /, which should probably be moved to their own file.

@[simp]

theorem Nat.mul_lt_mul_left {a b c : Nat} (a0 : 0 < a) : a * b < a * c ↔ b < c

@[simp]

theorem Nat.mul_lt_mul_right {a b c : Nat} (a0 : 0 < a) : b * a < c * a ↔ b < c

theorem Nat.lt_of_mul_lt_mul_left {a b c : Nat} (h : a * b < a * c) : b < c

theorem Nat.lt_of_mul_lt_mul_right {a b c : Nat} (h : b * a < c * a) : b < c

theorem Nat.div_lt_of_lt_mul {m n k : Nat} (h : m < n * k) : m / n < k

theorem Nat.mod_mul_right_div_self (m n k : Nat) : m % (n * k) / n = m / n % k

theorem Nat.mod_mul_left_div_self (m n k : Nat) : m % (k * n) / n = m / n % k

@[simp]

theorem Nat.mod_mul_right_mod (a b c : Nat) : a % (b * c) % b = a % b

@[simp]

theorem Nat.mod_mul_left_mod (a b c : Nat) : a % (b * c) % c = a % c

theorem Nat.mod_mul {a b x : Nat} : x % (a * b) = x % a + a * (x / a % b)

theorem Nat.mod_pow_succ {x b k : Nat} : x % b ^ (k + 1) = x % b ^ k + b ^ k * (x / b ^ k % b)

@[simp]

theorem Nat.two_pow_mod_two_eq_zero {n : Nat} : 2 ^ n % 2 = 0 ↔ 0 < n

@[simp]

theorem Nat.two_pow_mod_two_eq_one {n : Nat} : 2 ^ n % 2 = 1 ↔ n = 0