Commit c5fa19c8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added Rplsu_eq_reg_r.

parent f3c3f037
......@@ -51,11 +51,11 @@ rewrite H.
now destruct (Rcase_abs y) as [_|_] ; [right|left].
Qed.
Theorem Rabs_Rminus_pos:
forall x y : R,
(0 <= y)%R -> (y <= 2*x)%R ->
(Rabs (x-y) <= x)%R.
Proof.
intros x y Hx Hy.
unfold Rabs; case (Rcase_abs (x - y)); intros H.
apply Rplus_le_reg_l with x; ring_simplify; assumption.
......@@ -63,6 +63,14 @@ apply Rplus_le_reg_l with (-x)%R; ring_simplify.
auto with real.
Qed.
Theorem Rplus_eq_reg_r :
forall r r1 r2 : R,
(r1 + r = r2 + r)%R -> (r1 = r2)%R.
Proof.
intros r r1 r2 H.
apply Rplus_eq_reg_l with r.
now rewrite 2!(Rplus_comm r).
Qed.
Theorem Rplus_le_reg_r :
forall r r1 r2 : R,
......
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