match b with
| 0 => simp
| b + 1 =>
  match c with
  | 0 => simp[Nat.div_add_mod]
  | c + 1 =>
    apply Eq.trans
    apply congrArg₂ _ (Nat.div_add_mod a (b + 1)).symm rfl
    apply Eq.trans
    apply Nat.add_mod
    apply Eq.trans
    exact congrArg₂ _ (congrArg₂ _ (Nat.mul_mod_mul_left _ _ _) (Nat.mod_eq_of_lt (lt_of_lt_of_le (Nat.mod_lt _ (Nat.zero_lt_succ _)) (Nat.le_mul_of_pos_right (Nat.zero_lt_succ _))))) rfl
    apply Nat.mod_eq_of_lt
    apply Nat.lt_of_succ_le
    apply le_trans
    apply Nat.succ_le_succ
    apply add_le_add
    apply Nat.mul_le_mul_left
    apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
    apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
    simp [Nat.succ_eq_add_one, left_distrib, right_distrib, ← add_assoc]
a b c : ℕ
⊢ a % (b * c) = b * (a / b % c) + a % b
no goals