ワウさんが言ってたもの 任意の2以上の整数mと、任意の整数nについて、m|nかつm|n+1であることはない

wausan.v

Module Wau_san.
Require Import ZArith.
Theorem wau_san : (forall m n, (m > 1) -> ~ ((m | n) /\ (m | n+1)))%Z.
Proof.
intros m n Hm H.
destruct H as [Hmn Hm1n].
assert (H : (m | n+1 - n)%Z) by (apply Z.divide_sub_r; assumption).
replace (n+1 - n)%Z with 1%Z in H by ring.
apply Z.divide_1_r in H.
destruct H as [H|H]; subst; inversion Hm.
Qed.
End Wau_san.