proposition: Lemma div_mul_undo_le: forall a b, 0 <= a -> 0 < b -> a / b * b <= a.
proof: Proof. intros. pose proof (Zmod_eq_full a b) as P. pose proof (Z.mod_bound_pos a b) as Q. lia. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith