proposition: Lemma div_mul_undo: forall a b, b <> 0 -> a mod b = 0 -> a / b * b = a.
proof: Proof. intros. pose proof Z.div_mul_cancel_l as A. specialize (A a 1 b). replace (b * 1) with b in A by lia. rewrite Z.div_1_r in A. rewrite Z.mul_comm. rewrite <- Z.divide_div_mul_exact; try assumption. - apply A; congruence. - apply Z.mod_divide; assumption. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith