proposition: Lemma Rabs_add : forall x y, x >= 0 -> 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]] ; [lra|idtac|idtac]) ; (destruct (Rcase_abs (y)) as [H3|[H3|H3]] ; [lra|idtac|idtac]) ; (destruct (Rcase_abs (x + y)) as [H4|[H4|H4]] ; [lra|ring|ring]). Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions