proposition: Lemma Zneg_xI_IZR : forall x, IZR (Zneg (xI x)) = (R1 + R1) * IZR (Zneg x) - R1.
proof: Proof. intros x. rewrite Zneg_xI. unfold Zminus. rewrite plus_IZR. rewrite mult_IZR. rewrite Ropp_Ropp_IZR. simpl. ring. Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions