proposition: Theorem Fabs_correct2 : forall x : float, (FtoR radix x <= 0)%R -> Fabs x = (- x)%R :>R.
proof: Proof. intros x; case x; unfold FtoRradix, FtoR in |- *; simpl in |- *. intros Fnum1 Fexp1 H'. rewrite <- Ropp_mult_distr_l_reverse; repeat rewrite <- (Rmult_comm (powerRZ radix Fexp1)); apply Rmult_eq_compat_l; auto. cut (Fnum1 <= 0)%Z. intros; rewrite Z.abs_neq; try assumption. now rewrite opp_IZR. apply Znot_gt_le. contradict H'. apply Rgt_not_le; auto. rewrite Rmult_comm. replace 0%R with (powerRZ radix Fexp1 * 0)%R; auto with real. red in |- *; apply Rmult_lt_compat_l; auto with real arith. replace 0%R with (IZR 0); auto with real zarith arith. now apply powerRZ_lt, IZR_lt. apply IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz