Commit 5c7b0225 authored by Heiko Becker's avatar Heiko Becker

Move some lemmas

parent 2e3aaa7d
......@@ -165,31 +165,6 @@ Proof.
unfold Qle_bool; auto.
Qed.
Lemma minAbs_positive_iv_is_lo a b:
(0 < a)%R ->
(a <= b)%R ->
RminAbsFun (a,b) = a.
Proof.
intros; unfold RminAbsFun; simpl.
assert (0 < b)%R by lra.
assert (Rabs a = a)%R as Rabs_pos_a by (apply Rabs_right; lra).
assert (Rabs b = b)%R as Rabs_pos_b by (apply Rabs_right; lra).
rewrite Rabs_pos_a, Rabs_pos_b.
rewrite Rmin_left; lra.
Qed.
Lemma minAbs_negative_iv_is_hi a b:
(b < 0)%R ->
(a <= b)%R ->
(RminAbsFun (a,b) = - b)%R.
Proof.
intros; unfold RminAbsFun; simpl.
assert (Rabs a = - a)%R as Rabs_neg_a by (apply Rabs_left; lra).
assert (Rabs b = - b)%R as Rabs_neg_b by (apply Rabs_left; lra).
rewrite Rabs_neg_a, Rabs_neg_b.
rewrite Rmin_right; lra.
Qed.
Lemma Q_case_div_to_R_case_div a b:
(b < 0 \/ 0 < a)%Q ->
(Q2R b < 0 \/ 0 < Q2R a)%R.
......
......@@ -347,4 +347,30 @@ Proof.
rewrite Rabs_minus_sym in abs_le.
unfold Rabs in abs_le.
destruct Rcase_abs in abs_le; try lra.
Qed.
Lemma minAbs_positive_iv_is_lo a b:
(0 < a)%R ->
(a <= b)%R ->
RminAbsFun (a,b) = a.
Proof.
intros; unfold RminAbsFun; simpl.
assert (0 < b)%R by lra.
assert (Rabs a = a)%R as Rabs_pos_a by (apply Rabs_right; lra).
assert (Rabs b = b)%R as Rabs_pos_b by (apply Rabs_right; lra).
rewrite Rabs_pos_a, Rabs_pos_b.
rewrite Rmin_left; lra.
Qed.
Lemma minAbs_negative_iv_is_hi a b:
(b < 0)%R ->
(a <= b)%R ->
(RminAbsFun (a,b) = - b)%R.
Proof.
intros; unfold RminAbsFun; simpl.
assert (Rabs a = - a)%R as Rabs_neg_a by (apply Rabs_left; lra).
assert (Rabs b = - b)%R as Rabs_neg_b by (apply Rabs_left; lra).
rewrite Rabs_neg_a, Rabs_neg_b.
rewrite Rmin_right; lra.
Qed.
\ No newline at end of file
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