proposition: Lemma Rabs_minus : forall x y, x >= 0 -> 0 >= y -> Rabs (x - y) = Rabs x + Rabs y.
proof: Proof. intros x y H H1. unfold Rabs. (destruct (Rcase_abs (x)) as [H2|[H2|H2]] ; [lra|idtac|idtac]) ; (destruct (Rcase_abs (y)) as [H3|[H3|H3]] ; [idtac|lra|idtac]) ; (destruct (Rcase_abs (x - y)) as [H4|[H4|H4]] ; [lra|idtac|idtac]). ring. ring. rewrite H3. ring. rewrite H3. ring. ring. ring. rewrite H3. ring. rewrite H3. rewrite H2. ring. Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions