proposition: Lemma div_plus_compat : forall a b c : nat, Divides a b -> Divides a c -> Divides a (b + c).
proof: Proof. intros. elim H. intro x. intros. elim H0. intro y. intros. split with (x + y). rewrite H1. rewrite H2. symmetry in |- *. rewrite (mult_comm a). rewrite (mult_comm a). rewrite (mult_comm a). apply mult_plus_distr_r. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp