proposition: Lemma eqmod_div m a b : m <> 0 -> a <= b -> a mod m = b mod m <-> (m | b - a).
proof: Proof. intros mz l; split. - intros e. exists ((b / m) - (a / m)). rewrite Nat.mul_comm, Nat.mul_sub_distr_l. rewrite (Nat.div_mod a m mz) at 1. rewrite (Nat.div_mod b m mz) at 1. lia. - intros (k, e). assert (b = a + k * m) by lia. assert (b mod m = (a + k * m) mod m) as -> by congruence. rewrite Nat.mod_add; auto. Qed.
imports: Coq(Arith Euclid Compare Lia)