add_zero'

formal source

 379theorem zero_add' (a : LogicInt) : (0 : LogicInt) + a = a := by
 380  rw [eq_iff_toInt_eq, toInt_add, toInt_zero]; ring
 381
 382theorem add_zero' (a : LogicInt) : a + (0 : LogicInt) = a := by
 383  rw [eq_iff_toInt_eq, toInt_add, toInt_zero]; ring
 384
 385theorem add_left_neg' (a : LogicInt) : -a + a = 0 := by
 386  rw [eq_iff_toInt_eq, toInt_add, toInt_neg, toInt_zero]; ring
 387
 388theorem mul_assoc' (a b c : LogicInt) : (a * b) * c = a * (b * c) := by
 389  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul, toInt_mul, toInt_mul]; ring
 390
 391theorem mul_comm' (a b : LogicInt) : a * b = b * a := by
 392  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul]; ring
 393
 394theorem one_mul' (a : LogicInt) : (1 : LogicInt) * a = a := by
 395  rw [eq_iff_toInt_eq, toInt_mul, toInt_one]; ring
 396
 397theorem mul_one' (a : LogicInt) : a * (1 : LogicInt) = a := by
 398  rw [eq_iff_toInt_eq, toInt_mul, toInt_one]; ring
 399
 400theorem mul_add' (a b c : LogicInt) : a * (b + c) = a * b + a * c := by
 401  rw [eq_iff_toInt_eq, toInt_mul, toInt_add, toInt_add, toInt_mul, toInt_mul]; ring
 402
 403theorem add_mul' (a b c : LogicInt) : (a + b) * c = a * c + b * c := by
 404  rw [eq_iff_toInt_eq, toInt_mul, toInt_add, toInt_add, toInt_mul, toInt_mul]; ring
 405
 406/-- `LogicInt` has no zero divisors: from `a * b = 0`, either `a = 0`
 407or `b = 0`. Forced by the ring isomorphism with `Int`. -/
 408theorem mul_eq_zero {a b : LogicInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 409  constructor
 410  · intro h
 411    have hint : toInt a * toInt b = 0 := by
 412      rw [← toInt_mul]