diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Coqlib.v | 6 | ||||
| -rw-r--r-- | lib/Iteration.v | 3 |
2 files changed, 7 insertions, 2 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 045fb03a..9b8f2abb 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -406,6 +406,12 @@ Qed. (** Properties of Euclidean division and modulus. *) +Lemma Z_div_mod_eq: forall a b, + b > 0 -> a = (b * (a / b) + a mod b). +Proof. + intros. apply Z.div_mod. lia. +Qed. + Lemma Zmod_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x mod y = b. diff --git a/lib/Iteration.v b/lib/Iteration.v index 34471826..50672069 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -204,7 +204,6 @@ End PrimIter. Require Import Classical. Require Import ClassicalDescription. -Require Import Max. Module GenIter. @@ -280,7 +279,7 @@ Lemma converges_to_unique: Proof. intros a b [n C] b' [n' C']. rewrite <- (C (max n n')). rewrite <- (C' (max n n')). auto. - apply le_max_r. apply le_max_l. + apply Nat.le_max_r. apply Nat.le_max_l. Qed. Lemma converges_to_exists_uniquely: |