proposition: Lemma Rabs_Rinv_neg : forall x, 0 > x -> Rabs (/x) = - / x.
proof: Proof. intros x H. assert (H0 : ( x <> 0)). intro H1. rewrite H1 in H. lra. rewrite Rabs_inv. rewrite Rabs_left. field. assumption. intuition. Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions