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