diff options
Diffstat (limited to 'theories/NArith/Ndist.v')
| -rw-r--r-- | theories/NArith/Ndist.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 0b61718f8..9d399f5cd 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -301,7 +301,7 @@ Proof. cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false). intros. apply H1. reflexivity. intro a''. case a''. intro. reflexivity. - intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). unfold xorf in |- *. + intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). rewrite (Nplength_zeros (Npos p) (Pplength p) (refl_equal (Nplength (Npos p))) k H0). |