proposition: Lemma Zdivide_inf : forall a b, (a | b) -> { q | b = q * a }.
proof: Proof. intros a b D. exists (b / a). rewrite Zmult_comm. destruct (Z.eq_dec a 0). subst; destruct D; lia. apply Z_div_exact_full_2; auto with *. apply Zdivide_mod; auto. Defined.
imports: ZArith Lia Znumtheory