You should have included some information about what you've tried so far or how you would prove it if you knew what tactics to use.
Here are some ideas. I bet most of these have already been proven. Use the SearchAbout
and SearchPattern
commands to find the name of the proofs. This comes without warranty.
Require Import Coq.Reals.Reals.
Conjecture C01 : forall p1, True /\ p1 <-> p1.
Conjecture C02 : forall r1 r2 r3, (r1 + (r2 + r3))%R = (r1 + r2 + r3)%R.
Conjecture C03 : forall r1 r2, (r1 + - r2)%R = (r1 - r2)%R.
Conjecture C04 : forall r1, (0 - r1)%R = (- r1)%R.
Conjecture C05 : forall r1, (r1 - 0)%R = r1.
Conjecture C06 : forall r1 r2, (r1 + r2 - r2)%R = r1%R.
Conjecture C07 : forall r1, (1 * r1)%R = r1.
Conjecture C08 : forall r1 r2 r3, ((r1 + r2) * r3)%R = (r1 * r3 + r2 * r3)%R.
Conjecture C09 : forall r1, (r1 <= r1 + 1)%R <-> True.
Conjecture C10 : forall r1 r2, ~ (r1 <= r2)%R <-> (r2 < r1)%R.
Conjecture C11 : forall r1 r2 r3, (r1 + r3 < r2 + r3)%R <-> (r1 < r2)%R.
Hint Rewrite C01 C02 C03 C04 C05 C06 C07 C08 C09 C10 C11 : Hints.
Conjecture C12 : forall r1, (r1 < r1 + 1)%R.
Conjecture C13 : forall r1 r2, (r1 < r2)%R -> (r1 < r2 + 1)%R.
Hint Resolve C12 C13 : Hints.
Goal ~ ((1 <= 2 - 0)%R /\ (5 <= 2 + 1 + ( 0 - 1))%R).
Proof. autorewrite with Hints. eauto with Hints. Qed.