proposition: Lemma not_divides_plus : forall n m:nat, ~ divides n m -> ~ divides n (n+m).
proof: Proof. intros n m H; red; intro H'; elim H'; intro y. case y; simpl. intro H2; apply H. cut (m=0). intro H3; rewrite H3; apply divides_O. lia. intros n0 Hn0. apply H. exists n0. lia. Qed.
imports: Arith Lia