diff options
Diffstat (limited to 'flocq/Prop/Fprop_Sterbenz.v')
| -rw-r--r-- | flocq/Prop/Fprop_Sterbenz.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Prop/Fprop_Sterbenz.v b/flocq/Prop/Fprop_Sterbenz.v index 7260d2e1..4e74f889 100644 --- a/flocq/Prop/Fprop_Sterbenz.v +++ b/flocq/Prop/Fprop_Sterbenz.v @@ -133,7 +133,7 @@ assert (Hy0: (0 <= y)%R). apply Rplus_le_reg_r with y. apply Rle_trans with x. now rewrite Rplus_0_l. -now rewrite Rmult_plus_distr_r, Rmult_1_l in Hxy2. +now replace (y + y)%R with (2 * y)%R by ring. rewrite Rabs_pos_eq with (1 := Hy0). rewrite Rabs_pos_eq. unfold Rmin. |