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