proposition: Theorem Fplus_correct : forall x y : float, Fplus x y = (x + y)%R :>R.
proof: Proof. intros x y; unfold Fplus, Fshift, FtoRradix, FtoR in |- *; simpl in |- *. rewrite plus_IZR. rewrite Rmult_comm; rewrite Rmult_plus_distr_l; auto. repeat rewrite mult_IZR. repeat rewrite (Rmult_comm (Fnum x)); repeat rewrite (Rmult_comm (Fnum y)). repeat rewrite Zpower_nat_Z_powerRZ; auto. repeat rewrite <- Rmult_assoc. repeat rewrite <- powerRZ_add; auto with real zarith arith. 2: now apply Rgt_not_eq, IZR_lt. 2: now apply Rgt_not_eq, IZR_lt. repeat rewrite inj_abs; try lia. repeat rewrite Zplus_minus; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz