Commit 5b2b4140 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Prepare for removal of inequalities with both sides varying.

parent 6573e072
......@@ -54,6 +54,7 @@ Goal
x < 1 + powerRZ x 3.
Proof.
intros.
apply Rminus_lt.
interval with (i_bisect_diff x).
Qed.
......
......@@ -2,21 +2,28 @@ Require Import Reals.
Require Import Interval.Tactic.
Goal forall x, (1 <= x)%R -> (0 < x)%R.
Proof.
intros.
interval.
Qed.
Goal forall x, (1 <= x)%R -> (x <= x * x)%R.
Proof.
intros.
apply Rminus_le.
interval with (i_bisect_diff x).
Qed.
Goal forall x, (2 <= x)%R -> (x < x * x)%R.
Proof.
intros.
apply Rminus_lt.
interval with (i_bisect_diff x).
Qed.
Goal forall x, (-1 <= x)%R -> (x < 1 + powerRZ x 3)%R.
Proof.
intros.
apply Rminus_lt.
interval with (i_bisect_diff x).
Qed.
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