diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-04 18:48:06 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-04 18:48:06 +0000 |
| commit | 12c796fe185876021e2dfc7753b8f90ba9de31e0 (patch) | |
| tree | 38eea7388cb9295f2169ad34eb1682578017aaee /theories/Numbers/Natural/BigN/NMake.v | |
| parent | fdda04b92b7347f252d41aa76693ec221a07fe47 (diff) | |
Ndigits: a Pshiftl_nat used in BigN (was double_digits there)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13764 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 105cf0620..23cfec5e9 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -64,7 +64,7 @@ Module Make (W0:CyclicType) <: NType. Proof. intros. change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))). - rewrite !digits_dom_op, !Pshiftl_Zpower. + rewrite !digits_dom_op, !Pshiftl_nat_Zpower. apply Zmult_le_compat_l; auto with zarith. apply Zpower_le_monotone2; auto with zarith. Qed. @@ -1050,7 +1050,7 @@ Module Make (W0:CyclicType) <: NType. unfold base. apply Zlt_le_trans with (1 := pheight_correct x). apply Zpower_le_monotone2; auto with zarith. - rewrite (digits_dom_op (_ _)), Pshiftl_Zpower. auto with zarith. + rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith. Qed. Definition of_N (x:N) : t := @@ -1392,7 +1392,7 @@ Module Make (W0:CyclicType) <: NType. forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)). Proof. intros x. rewrite ! digits_level, double_size_level. - rewrite 2 digits_dom_op, 2 Pshiftl_Zpower, + rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower, inj_S, Zpower_Zsucc; auto with zarith. ring. Qed. |