proposition: Lemma Zmod_divide_minus a b c: 0 < b -> a mod b = c -> (b | a - c).
proof: Proof. Proof with auto using Z_lt_neq. intros H H1. apply Z.mod_divide... rewrite Zminus_mod. rewrite H1. rewrite <- (Z.mod_small c b) at 1. - rewrite Z.sub_diag, Z.mod_0_l... - subst. now apply Z.mod_pos_bound. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat