proposition: Lemma plus_Int_part2 : forall r1 r2:R, frac_part r1 + frac_part r2 < 1 -> Int_part (r1 + r2) = (Int_part r1 + Int_part r2)%Z.
proof: Proof. intros; elim (base_fp r1); elim (base_fp r2); intros; clear H1 H3; generalize (Rge_le (frac_part r2) 0 H0); intro; clear H0; generalize (Rge_le (frac_part r1) 0 H2); intro; clear H2; generalize (Rplus_le_compat_l (frac_part r1) 0 (frac_part r2) H1); intro; clear H1; elim (Rplus_ne (frac_part r1)); intros a b; rewrite a in H2; clear a b; generalize (Rle_trans 0 (frac_part r1) (frac_part r1 + frac_part r2) H0 H2); intro; clear H0 H2; unfold frac_part in H, H1; unfold Rminus in H, H1; rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2))) in H1; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H1; rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2) in H1; rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H1; rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2))) in H1; rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H1; rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2))) in H; rewrite (Rplus_comm r2 (- IZR (Int_part r2))) in H; rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2) in H; rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2) in H; rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2))) in H; rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))) in H; generalize (Rplus_le_compat_l (IZR (Int_part r1) + IZR (Int_part r2)) 0 (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) H1); intro; clear H1; generalize (Rplus_lt_compat_l (IZR (Int_part r1) + IZR (Int_part r2)) (r1 + r2 + - (IZR (Int_part r1) + IZR (Int_part r2))) 1 H); intro; clear H; rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2)))) in H1; rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2)) in H1; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H1; elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H1; clear a b; rewrite (Rplus_comm (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2)))) in H0; rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) (- (IZR (Int_part r1) + IZR (Int_part r2))) (r1 + r2)) in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0; elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2))); intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H0; clear a b. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); intro; clear H0 H1; unfold Int_part at 1. normZ. - slia H HZ. - slia H0 HZ. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac