Theorem: N2 (LeanTeaching/Ex2/3.lean)

State before:
a b c : ℤ
h1 : a ∣ b
h2 : a ∣ c
⊢ a ∣ b + c
Tactic:
sorry
State after:
no goals