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 b : ℕ
⊢ a % ((b + 1) * c) = (b + 1) * (a / (b + 1) % c) + a % (b + 1)
no goals