Library RInequalities
Require Export Reals.
Require Import ComhCoq.GenTacs.
Require Import ComhCoq.Extras.LibTactics.
Open Scope R_scope.
Ltac Rmult_le_zero :=
match goal with
| [ |- 0 <= ?y1 * ?y2] =>
replace 0 with (0 * 0);[ | ring];
apply Rmult_le_compat;[apply Rle_refl | apply Rle_refl | ..]
end.
Require Import ComhCoq.GenTacs.
Require Import ComhCoq.Extras.LibTactics.
Open Scope R_scope.
Ltac Rmult_le_zero :=
match goal with
| [ |- 0 <= ?y1 * ?y2] =>
replace 0 with (0 * 0);[ | ring];
apply Rmult_le_compat;[apply Rle_refl | apply Rle_refl | ..]
end.
Splits the goal into 2 subgoals based on d <= t or t < d
Ltac Rleltcases d t U := let H := fresh in lets H : Rle_or_lt d t;
let U1 := fresh U in elim_intro H U1 U1.
Lemma not_Rle_lt : forall (r1 r2 : R),
~r1 <= r2 -> r2 < r1.
Lemma RltMinusBothSides : forall (r1 r2 : R),
r2 < r1 -> 0 < (r1 - r2).
Ltac Rle_trans_red :=
match goal with
| [H1 : ?r1 <= ?r2, H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | apply H2]
| [H1 : ?r1 <= ?r2 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | ]
| [H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[ | apply H2]
end.
Ltac Rle_trans_rev_red :=
match reverse goal with
| [H1 : ?r1 <= ?r2, H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | apply H2]
| [H1 : ?r1 <= ?r2 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | ]
| [H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[ | apply H2]
end.
Ltac Rplus_le_cancel_middle :=
match goal with
| [ |- ?x1 + ?r + ?x2 <= ?y1 + ?r + ?y2] =>
replace (x1 + r + x2) with (x1 + x2 + r);[ | ring];
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_le_compat_r
| [ |- ?x1 + ?r <= ?y1 + ?r + ?y2] =>
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_le_compat_r
end.
Ltac Rle_ring_solve := apply Req_le; simpl; ring.
Ltac Rle_refl_solve := apply Rle_refl.
Lemma Rle_plus_r : forall (x y : R),
0 <= y -> x <= x + y.
Lemma Rle_plus_l : forall (x y : R),
0 <= y -> x <= y + x.
Lemma RleMinusBothSides : forall (r1 r2 : R),
r2 <= r1 -> 0 <= (r1 - r2).
Lemma Rmult_le_0_compat : forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
Lemma Rle_zero_plus : forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
Lemma Rle_zero_mult : forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
Lemma RlePlusExistsR : forall (r1 r2 : R),
r1 <= r2 -> exists r3, r2 = r1 + r3 /\ 0 <= r3.
Lemma RlePlusExistsL : forall (r1 r2 : R),
r1 <= r2 -> exists r3, r2 = r3 + r1 /\ 0 <= r3.
Lemma Rle_or_le : forall (r1 r2 : R), r1 <= r2 \/ r2 <= r1.
Lemma Rplus_le_swap_rr : forall (x y z : R),
x <= y + z -> x - z <= y.
Lemma Rplus_le_swap_rl : forall (x y z : R),
x <= y + z -> x - y <= z.
Lemma Rplus_le_swap_lr : forall (x y z : R),
x + y <= z -> x <= z - y.
Lemma Rplus_le_swap_ll : forall (x y z : R),
x + y <= z -> y <= z - x.
Lemma Rminus_le_swap_rr : forall (x y z : R),
x <= y - z -> x + z <= y.
Lemma Rminus_le_swap_lr : forall (x y z : R),
x - y <= z -> x <= z + y.
Lemma Rplus_le_weaken_lr : forall (x y z : R), x + y <= z -> 0 <= y -> x <= z.
Lemma Rplus_le_weaken_ll : forall (x y z : R), x + y <= z -> 0 <= x -> y <= z.
Lemma Rplus_le_weaken_rr : forall (x y z : R), 0 <= z -> x <= y -> x <= y + z.
Lemma Rplus_le_weaken_rl : forall (x y z : R), 0 <= y -> x <= z -> x <= y + z.
Lemma Rminus_le_weaken_lr : forall (x y z : R), 0 <= y -> x <= z -> x - y <= z.
let U1 := fresh U in elim_intro H U1 U1.
Lemma not_Rle_lt : forall (r1 r2 : R),
~r1 <= r2 -> r2 < r1.
Lemma RltMinusBothSides : forall (r1 r2 : R),
r2 < r1 -> 0 < (r1 - r2).
Ltac Rle_trans_red :=
match goal with
| [H1 : ?r1 <= ?r2, H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | apply H2]
| [H1 : ?r1 <= ?r2 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | ]
| [H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[ | apply H2]
end.
Ltac Rle_trans_rev_red :=
match reverse goal with
| [H1 : ?r1 <= ?r2, H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | apply H2]
| [H1 : ?r1 <= ?r2 |- ?r1 <= ?r3] =>
eapply Rle_trans;[apply H1 | ]
| [H2 : ?r2 <= ?r3 |- ?r1 <= ?r3] =>
eapply Rle_trans;[ | apply H2]
end.
Ltac Rplus_le_cancel_middle :=
match goal with
| [ |- ?x1 + ?r + ?x2 <= ?y1 + ?r + ?y2] =>
replace (x1 + r + x2) with (x1 + x2 + r);[ | ring];
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_le_compat_r
| [ |- ?x1 + ?r <= ?y1 + ?r + ?y2] =>
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_le_compat_r
end.
Ltac Rle_ring_solve := apply Req_le; simpl; ring.
Ltac Rle_refl_solve := apply Rle_refl.
Lemma Rle_plus_r : forall (x y : R),
0 <= y -> x <= x + y.
Lemma Rle_plus_l : forall (x y : R),
0 <= y -> x <= y + x.
Lemma RleMinusBothSides : forall (r1 r2 : R),
r2 <= r1 -> 0 <= (r1 - r2).
Lemma Rmult_le_0_compat : forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
Lemma Rle_zero_plus : forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
Lemma Rle_zero_mult : forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
Lemma RlePlusExistsR : forall (r1 r2 : R),
r1 <= r2 -> exists r3, r2 = r1 + r3 /\ 0 <= r3.
Lemma RlePlusExistsL : forall (r1 r2 : R),
r1 <= r2 -> exists r3, r2 = r3 + r1 /\ 0 <= r3.
Lemma Rle_or_le : forall (r1 r2 : R), r1 <= r2 \/ r2 <= r1.
Lemma Rplus_le_swap_rr : forall (x y z : R),
x <= y + z -> x - z <= y.
Lemma Rplus_le_swap_rl : forall (x y z : R),
x <= y + z -> x - y <= z.
Lemma Rplus_le_swap_lr : forall (x y z : R),
x + y <= z -> x <= z - y.
Lemma Rplus_le_swap_ll : forall (x y z : R),
x + y <= z -> y <= z - x.
Lemma Rminus_le_swap_rr : forall (x y z : R),
x <= y - z -> x + z <= y.
Lemma Rminus_le_swap_lr : forall (x y z : R),
x - y <= z -> x <= z + y.
Lemma Rplus_le_weaken_lr : forall (x y z : R), x + y <= z -> 0 <= y -> x <= z.
Lemma Rplus_le_weaken_ll : forall (x y z : R), x + y <= z -> 0 <= x -> y <= z.
Lemma Rplus_le_weaken_rr : forall (x y z : R), 0 <= z -> x <= y -> x <= y + z.
Lemma Rplus_le_weaken_rl : forall (x y z : R), 0 <= y -> x <= z -> x <= y + z.
Lemma Rminus_le_weaken_lr : forall (x y z : R), 0 <= y -> x <= z -> x - y <= z.
Tries to solve an inequality on real numbers.
Ltac Rplus_le_tac :=
match goal with
| [ H1 : ?r1 <= ?r3, H2 : ?r2 <= ?r4 |- ?r1 + ?r2 <= ?r3 + ?r4] =>
apply Rplus_le_compat;[apply H1 | apply H2]
| [ H1 : ?r1 <= ?r3, H2 : ?r2 <= ?r4 |- ?r2 + ?r1 <= ?r3 + ?r4] =>
rewrite Rplus_comm; apply Rplus_le_compat;[apply H1 | apply H2]
| [ H1 : ?r1 <= ?r2|- ?r + ?r1 <= ?r + ?r2] =>
apply Rplus_le_compat_l;apply H1
| [ H1 : ?r1 <= ?r2|- ?r1 + ?r <= ?r2 + ?r] =>
apply Rplus_le_compat_r;apply H1
| [ |- ?r + ?r1 <= ?r + ?r2] =>
apply Rplus_le_compat_l
| [ |- ?r1 + ?r <= ?r2 + ?r] =>
apply Rplus_le_compat_r
| [ H : ?r1 + ?r <= ?r2 + ?r |- ?r1 <= ?r2] =>
apply Rplus_le_reg_l in H; assumption
| [ H : ?r + ?r1 <= ?r + ?r2 |- ?r1 <= ?r2] =>
apply Rplus_le_reg_r in H; assumption
| [ H : ?x <= ?y + ?z |- ?x - ?z <= ?y] =>
apply Rplus_le_swap_rr; assumption
| [ H : ?x + ?y <= ?z |- ?y <= ?z - ?x] =>
apply Rplus_le_swap_ll; assumption
| [ H : ?x + ?y <= ?z |- ?x <= ?z - ?y] =>
apply Rplus_le_swap_lr; assumption
| [ H : ?x <= ?y + ?z |- ?x - ?y <= ?z] =>
apply Rplus_le_swap_rl; assumption
| [ |- ?r1 <= ?r1 + _] => apply Rle_plus_r
| [ |- ?r1 <= _ + ?r1] => apply Rle_plus_l
| [ H : ?x + ?y <= ?z |- ?x <= ?z] =>
eapply Rplus_le_weaken_lr; apply H
| [ H : ?x + ?y <= ?z |- ?y <= ?z] =>
eapply Rplus_le_weaken_ll; apply H
end.
Ltac Rlt_trans_red :=
match goal with
| [H1 : ?r1 < ?r2, H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | apply H2]
| [H1 : ?r1 < ?r2 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | ]
| [H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[ | apply H2]
end.
Ltac Rlt_trans_rev_red :=
match reverse goal with
| [H1 : ?r1 < ?r2, H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | apply H2]
| [H1 : ?r1 < ?r2 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | ]
| [H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[ | apply H2]
end.
Ltac Rplus_lt_cancel_middle :=
match goal with
| [ |- ?x1 + ?r + ?x2 < ?y1 + ?r + ?y2] =>
replace (x1 + r + x2) with (x1 + x2 + r);[ | ring];
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_lt_compat_r
| [ |- ?x1 + ?r < ?y1 + ?r + ?y2] =>
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_lt_compat_r
end.
Lemma Rlt_plus_r : forall (x y : R),
0 < y -> x < x + y.
Lemma Rlt_plus_l : forall (x y : R),
0 < y -> x < y + x.
Lemma Rlt_zero_plus : forall r1 r2 : R,
0 < r1 -> 0 < r2 -> 0 < r1 + r2.
Lemma RltPlusExistsR : forall (r1 r2 : R),
r1 < r2 -> exists r3, r2 = r1 + r3 /\ 0 < r3.
Lemma RltPlusExistsL : forall (r1 r2 : R),
r1 < r2 -> exists r3, r2 = r3 + r1 /\ 0 < r3.
Lemma RltExistsBetween (r1 r2 : R) : r1 < r2 -> exists r3,
r1 < r3 < r2.
Lemma Rplus_lt_swap_rl : forall (x y z : R),
x < y + z -> x - y < z.
Lemma Rplus_lt_swap_rr : forall (x y z : R),
x < y + z -> x - z < y.
Lemma Rplus_lt_swap_ll : forall (x y z : R),
x + y < z -> y < z - x.
Lemma Rplus_lt_swap_lr : forall (x y z : R),
x + y < z -> x < z - y.
Lemma Rminus_lt_swap_rr : forall (x y z : R),
x < y - z -> x + z < y.
Lemma Rminus_lt_swap_lr : forall (x y z : R),
x - y < z -> x < z + y.
Lemma Rplus_lt_reg_l: forall r r1 r2 : R, r1 + r < r2 + r -> r1 < r2.
Lemma Rplus_lt_reg_r: forall r r1 r2 : R, r + r1 < r + r2 -> r1 < r2.
Lemma Rplus_lt_weaken_lr : forall (x y z : R), x + y < z -> 0 <= y -> x < z.
Lemma Rplus_lt_weaken_ll : forall (x y z : R), x + y < z -> 0 <= x -> y < z.
Lemma Rplus_lt_weaken_rr : forall (x y z : R), 0 <= z -> x < y -> x < y + z.
Lemma Rplus_lt_weaken_rl : forall (x y z : R), 0 <= y -> x < z -> x < y + z.
Lemma Rminus_lt_weaken_lr : forall (x y z : R), 0 <= y -> x < z -> x - y < z.
match goal with
| [ H1 : ?r1 <= ?r3, H2 : ?r2 <= ?r4 |- ?r1 + ?r2 <= ?r3 + ?r4] =>
apply Rplus_le_compat;[apply H1 | apply H2]
| [ H1 : ?r1 <= ?r3, H2 : ?r2 <= ?r4 |- ?r2 + ?r1 <= ?r3 + ?r4] =>
rewrite Rplus_comm; apply Rplus_le_compat;[apply H1 | apply H2]
| [ H1 : ?r1 <= ?r2|- ?r + ?r1 <= ?r + ?r2] =>
apply Rplus_le_compat_l;apply H1
| [ H1 : ?r1 <= ?r2|- ?r1 + ?r <= ?r2 + ?r] =>
apply Rplus_le_compat_r;apply H1
| [ |- ?r + ?r1 <= ?r + ?r2] =>
apply Rplus_le_compat_l
| [ |- ?r1 + ?r <= ?r2 + ?r] =>
apply Rplus_le_compat_r
| [ H : ?r1 + ?r <= ?r2 + ?r |- ?r1 <= ?r2] =>
apply Rplus_le_reg_l in H; assumption
| [ H : ?r + ?r1 <= ?r + ?r2 |- ?r1 <= ?r2] =>
apply Rplus_le_reg_r in H; assumption
| [ H : ?x <= ?y + ?z |- ?x - ?z <= ?y] =>
apply Rplus_le_swap_rr; assumption
| [ H : ?x + ?y <= ?z |- ?y <= ?z - ?x] =>
apply Rplus_le_swap_ll; assumption
| [ H : ?x + ?y <= ?z |- ?x <= ?z - ?y] =>
apply Rplus_le_swap_lr; assumption
| [ H : ?x <= ?y + ?z |- ?x - ?y <= ?z] =>
apply Rplus_le_swap_rl; assumption
| [ |- ?r1 <= ?r1 + _] => apply Rle_plus_r
| [ |- ?r1 <= _ + ?r1] => apply Rle_plus_l
| [ H : ?x + ?y <= ?z |- ?x <= ?z] =>
eapply Rplus_le_weaken_lr; apply H
| [ H : ?x + ?y <= ?z |- ?y <= ?z] =>
eapply Rplus_le_weaken_ll; apply H
end.
Ltac Rlt_trans_red :=
match goal with
| [H1 : ?r1 < ?r2, H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | apply H2]
| [H1 : ?r1 < ?r2 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | ]
| [H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[ | apply H2]
end.
Ltac Rlt_trans_rev_red :=
match reverse goal with
| [H1 : ?r1 < ?r2, H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | apply H2]
| [H1 : ?r1 < ?r2 |- ?r1 < ?r3] =>
eapply Rlt_trans;[apply H1 | ]
| [H2 : ?r2 < ?r3 |- ?r1 < ?r3] =>
eapply Rlt_trans;[ | apply H2]
end.
Ltac Rplus_lt_cancel_middle :=
match goal with
| [ |- ?x1 + ?r + ?x2 < ?y1 + ?r + ?y2] =>
replace (x1 + r + x2) with (x1 + x2 + r);[ | ring];
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_lt_compat_r
| [ |- ?x1 + ?r < ?y1 + ?r + ?y2] =>
replace (y1 + r + y2) with (y1 + y2 + r);[ | ring];
apply Rplus_lt_compat_r
end.
Lemma Rlt_plus_r : forall (x y : R),
0 < y -> x < x + y.
Lemma Rlt_plus_l : forall (x y : R),
0 < y -> x < y + x.
Lemma Rlt_zero_plus : forall r1 r2 : R,
0 < r1 -> 0 < r2 -> 0 < r1 + r2.
Lemma RltPlusExistsR : forall (r1 r2 : R),
r1 < r2 -> exists r3, r2 = r1 + r3 /\ 0 < r3.
Lemma RltPlusExistsL : forall (r1 r2 : R),
r1 < r2 -> exists r3, r2 = r3 + r1 /\ 0 < r3.
Lemma RltExistsBetween (r1 r2 : R) : r1 < r2 -> exists r3,
r1 < r3 < r2.
Lemma Rplus_lt_swap_rl : forall (x y z : R),
x < y + z -> x - y < z.
Lemma Rplus_lt_swap_rr : forall (x y z : R),
x < y + z -> x - z < y.
Lemma Rplus_lt_swap_ll : forall (x y z : R),
x + y < z -> y < z - x.
Lemma Rplus_lt_swap_lr : forall (x y z : R),
x + y < z -> x < z - y.
Lemma Rminus_lt_swap_rr : forall (x y z : R),
x < y - z -> x + z < y.
Lemma Rminus_lt_swap_lr : forall (x y z : R),
x - y < z -> x < z + y.
Lemma Rplus_lt_reg_l: forall r r1 r2 : R, r1 + r < r2 + r -> r1 < r2.
Lemma Rplus_lt_reg_r: forall r r1 r2 : R, r + r1 < r + r2 -> r1 < r2.
Lemma Rplus_lt_weaken_lr : forall (x y z : R), x + y < z -> 0 <= y -> x < z.
Lemma Rplus_lt_weaken_ll : forall (x y z : R), x + y < z -> 0 <= x -> y < z.
Lemma Rplus_lt_weaken_rr : forall (x y z : R), 0 <= z -> x < y -> x < y + z.
Lemma Rplus_lt_weaken_rl : forall (x y z : R), 0 <= y -> x < z -> x < y + z.
Lemma Rminus_lt_weaken_lr : forall (x y z : R), 0 <= y -> x < z -> x - y < z.
Tries to solve an inequality on real numbers.
Ltac Rplus_lt_tac :=
match goal with
| [ H1 : ?r1 < ?r3, H2 : ?r2 < ?r4 |- ?r1 + ?r2 < ?r3 + ?r4] =>
apply Rplus_lt_compat;[apply H1 | apply H2]
| [ H1 : ?r1 <= ?r3, H2 : ?r2 < ?r4 |- ?r1 + ?r2 < ?r3 + ?r4] =>
apply Rplus_le_lt_compat;[apply H1 | apply H2]
| [ H1 : ?r1 < ?r3, H2 : ?r2 <= ?r4 |- ?r1 + ?r2 < ?r3 + ?r4] =>
apply Rplus_lt_le_compat;[apply H1 | apply H2]
| [ H1 : ?r1 < ?r3, H2 : ?r2 < ?r4 |- ?r2 + ?r1 < ?r3 + ?r4] =>
rewrite Rplus_comm; apply Rplus_lt_compat;[apply H1 | apply H2]
| [ H1 : ?r1 < ?r2|- ?r + ?r1 < ?r + ?r2] =>
apply Rplus_lt_compat_l;apply H1
| [ H1 : ?r1 < ?r2|- ?r1 + ?r < ?r2 + ?r] =>
apply Rplus_lt_compat_r;apply H1
| [ H : ?r1 + ?r < ?r2 + ?r |- ?r1 < ?r2] =>
apply Rplus_lt_reg_l in H; assumption
| [ H : ?r + ?r1 < ?r + ?r2 |- ?r1 < ?r2] =>
apply Rplus_lt_reg_r in H; assumption
| [ H : ?x < ?y + ?z |- ?x - ?z < ?y] =>
apply Rplus_lt_swap_rr; assumption
| [ H : ?x + ?y < ?z |- ?y < ?z - ?x] =>
apply Rplus_lt_swap_ll; assumption
| [ H : ?x < ?y + ?z |- ?x - ?y < ?z] =>
apply Rplus_lt_swap_rl; assumption
| [ H : ?x + ?y < ?z |- ?x < ?z - ?y] =>
apply Rplus_lt_swap_lr; assumption
| [ |- ?r1 < ?r1 + _] => apply Rlt_plus_r
| [ |- ?r1 < _ + ?r1] => apply Rlt_plus_l
| [ H : ?x + ?y < ?z |- ?x < ?z] =>
eapply Rplus_lt_weaken_lr; apply H
| [ H : ?x + ?y < ?z |- ?y < ?z] =>
eapply Rplus_lt_weaken_ll; apply H
end.
match goal with
| [ H1 : ?r1 < ?r3, H2 : ?r2 < ?r4 |- ?r1 + ?r2 < ?r3 + ?r4] =>
apply Rplus_lt_compat;[apply H1 | apply H2]
| [ H1 : ?r1 <= ?r3, H2 : ?r2 < ?r4 |- ?r1 + ?r2 < ?r3 + ?r4] =>
apply Rplus_le_lt_compat;[apply H1 | apply H2]
| [ H1 : ?r1 < ?r3, H2 : ?r2 <= ?r4 |- ?r1 + ?r2 < ?r3 + ?r4] =>
apply Rplus_lt_le_compat;[apply H1 | apply H2]
| [ H1 : ?r1 < ?r3, H2 : ?r2 < ?r4 |- ?r2 + ?r1 < ?r3 + ?r4] =>
rewrite Rplus_comm; apply Rplus_lt_compat;[apply H1 | apply H2]
| [ H1 : ?r1 < ?r2|- ?r + ?r1 < ?r + ?r2] =>
apply Rplus_lt_compat_l;apply H1
| [ H1 : ?r1 < ?r2|- ?r1 + ?r < ?r2 + ?r] =>
apply Rplus_lt_compat_r;apply H1
| [ H : ?r1 + ?r < ?r2 + ?r |- ?r1 < ?r2] =>
apply Rplus_lt_reg_l in H; assumption
| [ H : ?r + ?r1 < ?r + ?r2 |- ?r1 < ?r2] =>
apply Rplus_lt_reg_r in H; assumption
| [ H : ?x < ?y + ?z |- ?x - ?z < ?y] =>
apply Rplus_lt_swap_rr; assumption
| [ H : ?x + ?y < ?z |- ?y < ?z - ?x] =>
apply Rplus_lt_swap_ll; assumption
| [ H : ?x < ?y + ?z |- ?x - ?y < ?z] =>
apply Rplus_lt_swap_rl; assumption
| [ H : ?x + ?y < ?z |- ?x < ?z - ?y] =>
apply Rplus_lt_swap_lr; assumption
| [ |- ?r1 < ?r1 + _] => apply Rlt_plus_r
| [ |- ?r1 < _ + ?r1] => apply Rlt_plus_l
| [ H : ?x + ?y < ?z |- ?x < ?z] =>
eapply Rplus_lt_weaken_lr; apply H
| [ H : ?x + ?y < ?z |- ?y < ?z] =>
eapply Rplus_lt_weaken_ll; apply H
end.
Takes a hypothesis H of type r1 < r2 and gives a hypothesis U of type
r2 = r1 + d'
Ltac Rlttoplus H d' U := let Q1 := fresh in lets Q1 : RltPlusExistsL H;
let U1 := fresh U in let U2 := fresh U in decompExAnd Q1 d' U1 U2.
let U1 := fresh U in let U2 := fresh U in decompExAnd Q1 d' U1 U2.
This page has been generated by coqdoc