Commit 76f40788 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Removed unused theorems.

parent 9b0aee49
......@@ -414,83 +414,6 @@ Qed.
End Fcalc_bracket_step.
Section Fcalc_bracket_N.
Variable F : R -> Prop.
Variable d u x : R.
Hypothesis Hd : Rnd_DN_pt F x d.
Hypothesis Hu : Rnd_UP_pt F x u.
Theorem Rnd_N_pt_bracket_not_Hi :
forall l, l <> loc_Inexact Gt ->
inbetween d u x l ->
Rnd_N_pt F x d.
Proof.
intros l Hl Hx.
apply Rnd_DN_pt_N with (1 := Hd) (2 := Hu).
inversion Hx as [Hx'|l' Hx' Hl'].
rewrite Hx'.
unfold Rminus.
rewrite Rplus_opp_r.
apply Rle_0_minus.
apply Rle_trans with x.
apply Hd.
apply Hu.
apply Rcompare_not_Gt_inv.
rewrite Rcompare_middle.
rewrite Hl'.
contradict Hl.
now rewrite <- H, Hl.
Qed.
Theorem Rnd_N_pt_bracket_Mi_Hi :
forall l, l = loc_Inexact Eq \/ l = loc_Inexact Gt ->
inbetween d u x l ->
Rnd_N_pt F x u.
Proof.
intros l Hl Hx.
apply Rnd_UP_pt_N with (1 := Hd) (2 := Hu).
inversion Hx as [Hx' Hl'|l' Hx' Hl' Hl''].
now destruct Hl as [Hl|Hl] ; rewrite Hl in Hl'.
apply Rcompare_not_Lt_inv.
rewrite Rcompare_middle.
rewrite Hl'.
intros H.
rewrite H in Hl''.
rewrite <- Hl'' in Hl.
now destruct Hl.
Qed.
Theorem Rnd_not_N_pt_bracket_Hi :
inbetween d u x (loc_Inexact Gt) ->
~ Rnd_N_pt F x d.
Proof.
intros Hx (_, Hn).
specialize (Hn u (proj1 Hu)).
apply Rle_not_lt with (1 := Hn).
apply Rcompare_Gt_inv.
apply inbetween_distance_inexact_abs.
refine (let H := _ in Rlt_trans _ x _ (proj1 H) (proj2 H)).
now apply inbetween_bounds_not_Eq with (1 := Hx).
exact Hx.
Qed.
Theorem Rnd_not_N_pt_bracket_Lo :
inbetween d u x (loc_Inexact Lt) ->
~ Rnd_N_pt F x u.
Proof.
intros Hx (_, Hn).
specialize (Hn d (proj1 Hd)).
apply Rle_not_lt with (1 := Hn).
apply Rcompare_Lt_inv.
apply inbetween_distance_inexact_abs.
refine (let H := _ in Rlt_trans _ x _ (proj1 H) (proj2 H)).
now apply inbetween_bounds_not_Eq with (1 := Hx).
exact Hx.
Qed.
End Fcalc_bracket_N.
Section Fcalc_bracket_scale.
Lemma inbetween_mult_aux :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment