diff options
| -rw-r--r-- | theories/ZArith/Znat.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 6a82645ba6..7f72d42d1f 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -50,7 +50,7 @@ Qed. Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n. Proof. - destruct n; trivial. simpl. + destruct n as [|p]; trivial. simpl. destruct (Pos2Nat.is_succ p) as (m,H). rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv. Qed. @@ -668,7 +668,7 @@ Qed. Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z. Proof. - destruct z; simpl; trivial; + destruct z as [|p|p]; simpl; trivial; destruct (Pos2Nat.is_succ p) as (n,H); rewrite H; simpl; f_equal; now apply SuccNat2Pos.inv. Qed. |