From 2941378aee6586bcff9f8a117f11e5c5c2327607 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 28 Jun 2011 23:29:59 +0000 Subject: Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14244 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Numbers/Integer/Abstract') diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index f19baf4d16..0e54c453b7 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -88,7 +88,7 @@ Theorem div_unique_pos: Proof. intros; apply div_unique with r; auto. Qed. Theorem div_unique_neg: - forall a b q r, 0<=r a == b*q + r -> q == a/b. + forall a b q r, b a == b*q + r -> q == a/b. Proof. intros; apply div_unique with r; auto. Qed. Theorem mod_unique: -- cgit v1.2.3