proposition: Lemma IZR_POS_xI : forall p, IZR (Zpos (xI p)) = 1 + 2 * IZR (Zpos p).
proof: Proof. now unfold IZR, IPR; intros [p | p |]; simpl; try easy; rewrite Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField