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 in |- *; try split_case_Rabs; intros

  end.