proposition: Theorem Fabs_correct : forall x : float, Fabs x = Rabs x :>R.
proof: Proof. intros x; unfold Rabs in |- *. case (Rcase_abs x); intros H1. unfold FtoRradix in |- *; apply Fabs_correct2; auto with arith. apply Rlt_le; auto. unfold FtoRradix in |- *; apply Fabs_correct1; auto with arith. apply Rge_le; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz