proposition: Lemma Rrepr_INR : forall n : nat, CRealEq (Rrepr (INR n)) (inject_Z (Z.of_nat n)).
proof: Proof. induction n. - apply Rrepr_0. - replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z. + simpl. destruct n. * apply Rrepr_1. * rewrite Rrepr_plus,inject_Z_plus, <- IHn, Rrepr_1. reflexivity. + replace 1%Z with (Z.of_nat 1). * rewrite <- (Nat2Z.inj_add n 1). apply f_equal. rewrite Nat.add_comm. reflexivity. * reflexivity. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions