proposition: Lemma Z_div_mod' : forall a b : Z, Zdiv_hyp ((b > 0)%Z) -> let (q, r) := Z.div_eucl a b in a = (b * q)%I + r /\ (0 <= r < b)%Z.
proof: Proof. Proof using. applys Z_div_mod. Qed.
imports: Coq.micromega.Psatz TLC(LibTactics)