proposition: Lemma Zpos_xI_IZR : forall x, IZR (Zpos (xI x)) = (R1 + R1) * IZR (Zpos x) + R1.
proof: Proof. intros x. rewrite Zpos_xI. rewrite plus_IZR. rewrite mult_IZR. reflexivity. Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions