proposition: Lemma Int_part_INR : forall n:nat, Int_part (INR n) = Z.of_nat n.
proof: Proof. intros n; unfold Int_part. cut (up (INR n) = (Z.of_nat n + Z.of_nat 1)%Z). - intros H'; rewrite H'; simpl; ring. - symmetry; apply tech_up; auto. + replace (Z.of_nat n + Z.of_nat 1)%Z with (Z.of_nat (S n)). * repeat rewrite <- INR_IZR_INZ. apply lt_INR; auto. * rewrite Z.add_comm; rewrite <- Znat.Nat2Z.inj_add; simpl; auto. + rewrite plus_IZR; simpl; auto with real. repeat rewrite <- INR_IZR_INZ; auto with real. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac