proposition: Theorem FulpFabs : forall f : float, Fulp f = Fulp (Fabs f) :>R.
proof: Proof. intros f; unfold Fulp in |- *; case (Rle_or_lt 0 f); intros H'. replace (Fabs f) with f; auto; unfold Fabs in |- *; apply floatEq; simpl in |- *; auto with zarith real. apply sym_eq; apply Z.abs_eq; apply LeR0Fnum with radix; auto with zarith real. replace (Fabs f) with (Fopp f); [ rewrite Fnormalize_Fopp | apply floatEq; simpl in |- * ]; auto with zarith. apply sym_eq; apply Zabs_eq_opp; apply R0LeFnum with radix; auto with zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz