diff options
| -rw-r--r-- | contrib/omega/Zlogarithm.v | 3 | ||||
| -rw-r--r-- | contrib/omega/Zpower.v | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v index c5b36397f2..803981e332 100644 --- a/contrib/omega/Zlogarithm.v +++ b/contrib/omega/Zlogarithm.v @@ -14,6 +14,7 @@ (* (Log_nearest x) is the integer nearest from (Log x). *) (****************************************************************************) +Require ZArith. Require Omega. Require Zcomplements. Require Zpower. @@ -67,7 +68,9 @@ Definition log_inf_correct1 := Definition log_inf_correct2 := [p:positive](proj2 ? ? (log_inf_correct p)). +(***TODO: retablir les commandes Opaque / Transparent Opaque log_inf_correct1 log_inf_correct2. +***) Hints Resolve log_inf_correct1 log_inf_correct2 : zarith. Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`. diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v index d56e607d52..c696aec28c 100644 --- a/contrib/omega/Zpower.v +++ b/contrib/omega/Zpower.v @@ -344,7 +344,7 @@ Intros; Apply iter_pos_invariant with [ Intro; Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; [ Rewrite H0; Rewrite Zplus_assoc; Apply f_equal with f:=[z:Z]`z+r`; - Do 2 (Rewrite Zmult_plus_distr_l); + Do 2 '(Rewrite Zmult_plus_distr_l); Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p1) `2`); Rewrite <- Zplus_assoc; |