proposition: Lemma IZR_POS_xO : forall p, IZR (Zpos (p~0)) = 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