diff options
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZParity.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 0e9323789a..1e6593b101 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -95,7 +95,7 @@ Proof. intros. generalize (Even_or_Odd n) (Even_Odd_False n). rewrite <- even_spec, <- odd_spec. - destruct (odd n), (even n); simpl; intuition. + destruct (odd n), (even n) ; simpl; intuition. Qed. Lemma negb_even : forall n, negb (even n) = odd n. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 8146fd014f..6b6c853104 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -438,7 +438,7 @@ Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up. Proof. assert (Proper (eq==>eq==>Logic.eq) compare). intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. - intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx. + intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx. Qed. (** The spec of [sqrt_up] indeed determines it *) |