diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 10:26:26 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 11:33:55 +0200 |
commit | 76adb57c72fccb4f3e416bd7f3927f4fff72178b (patch) | |
tree | f8d72073a2ea62d3e5c274c201ef06532ac57b61 /theories/Reals/Ratan.v | |
parent | be01deca2b8ff22505adaa66f55f005673bf2d85 (diff) |
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Diffstat (limited to 'theories/Reals/Ratan.v')
-rw-r--r-- | theories/Reals/Ratan.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index dcf2f9709..6146b979f 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -450,9 +450,9 @@ fourier. Qed. Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}. -destruct (total_order_T (Rabs y) 1). - assert (yle1 : Rabs y <= 1) by (destruct s; fourier). - clear s; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. +destruct (total_order_T (Rabs y) 1) as [Hs|Hgt]. + assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier). + clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1. assert (0 < / (Rabs y + 1)). apply Rinv_0_lt_compat; fourier. @@ -530,7 +530,7 @@ split. assumption. replace (/(Rabs y + 1)) with (2 * u). fourier. - unfold u; field; apply Rgt_not_eq; clear -r; fourier. + unfold u; field; apply Rgt_not_eq; clear -Hgt; fourier. solve[discrR]. apply Rgt_not_eq; assumption. unfold tan. |