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