Library Coq.Reals.SplitAbsolu
Require Import Rbasic_fun.
Ltac split_case_Rabs :=
match goal with
| |-
context [(
Rcase_abs ?
X1)] =>
case (
Rcase_abs X1);
try split_case_Rabs
end.
Ltac split_Rabs :=
match goal with
|
id:
context [(
Rabs _)] |-
_ =>
generalize id;
clear id;
try split_Rabs
| |-
context [(
Rabs ?
X1)] =>
unfold Rabs;
try split_case_Rabs;
intros
end.