diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-17 15:40:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-17 15:40:49 +0200 |
| commit | 62b8190fd4b1c2223eb0a89329a28ca66d11a326 (patch) | |
| tree | bb1ada875c5a6c56c9a2f7270cb9876962a7a57d /theories/ZArith | |
| parent | c852523c11ca2d5edca6f35b12557e2d09dac1d6 (diff) | |
Revert "Essai où assert_style n'est utilisé que si pas visuellement une équation;" which was committed by mistake.
This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index be975e882..99b631905 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -54,17 +54,17 @@ Theorem Z_lt_abs_rec : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z * P (- z)). - enough (H:Q (Z.abs p)) by admit. -(* (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).*) + enough (H:Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). apply (Z_lt_rec Q); auto with zarith. subst Q; intros x H. split; apply HP. - rewrite Z.abs_eq; auto; intros. destruct (H (Z.abs m)); auto with zarith. - (* destruct (Zabs_dec m) as [-> | ->]; trivial. *) admit. + destruct (Zabs_dec m) as [-> | ->]; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial; admit. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. Theorem Z_lt_abs_induction : @@ -74,8 +74,8 @@ Theorem Z_lt_abs_induction : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. - enough (Q (Z.abs p)) by admit. -(* (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).*) + enough (Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). apply (Z_lt_induction Q); auto with zarith. subst Q; intros. split; apply HP. @@ -84,7 +84,7 @@ Proof. elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial; admit. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. (** To do case analysis over the sign of [z] *) |