proposition: Lemma not_divides_plus : forall n m:nat, ~divides n m -> ~divides n (n+m).
proof: Proof. intros n m H [q Hq]; apply H; red. destruct q. - exists 0. simpl in *. lia. - exists q; lia. Qed.
imports: ZArith List Arith Lia Reals Lra