From 12c796fe185876021e2dfc7753b8f90ba9de31e0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 4 Jan 2011 18:48:06 +0000 Subject: 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 --- theories/Numbers/Natural/BigN/NMake.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Numbers/Natural/BigN/NMake.v') 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. -- cgit v1.2.3