diff options
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 5a2c3cc32..dde0745eb 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -39,8 +39,8 @@ Proof. reflexivity. Qed. Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. Proof. unfold floor. induction p; simpl. - - rewrite !Z.pos_xI, (Z.pos_xO (xO _)), Z.pos_xO. omega. - - rewrite (Z.pos_xO (xO _)), (Z.pos_xO p), Z.pos_xO. omega. + - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. omega. + - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. omega. - omega. Qed. @@ -107,7 +107,7 @@ Require Import List. Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z := match l with | nil => acc - | _ :: l => Zlength_aux (Zsucc acc) A l + | _ :: l => Zlength_aux (Z.succ acc) A l end. Definition Zlength := Zlength_aux 0. |