proposition: Lemma IZR_Zpos_xI : forall p, IZR (Zpos (xI p)) = (1 + (1+1) * IZR (Zpos p))%R.
proof: Proof. intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)