proposition: Theorem Fabs_correct1 : forall x : float, (0 <= FtoR radix x)%R -> Fabs x = x :>R.
proof: Proof. intros x; case x; unfold FtoRradix, FtoR in |- *; simpl in |- *. intros Fnum1 Fexp1 H'. repeat rewrite <- (Rmult_comm (powerRZ radix Fexp1)); apply Rmult_eq_compat_l; auto. cut (0 <= Fnum1)%Z. unfold Z.abs, Z.le in |- *. case Fnum1; simpl in |- *; auto. intros p H'0; case H'0; auto. apply Znot_gt_le; auto. 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 zarith. apply powerRZ_lt, IZR_lt; easy. apply IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz