proposition: Theorem Fdigit_opp : forall x : float, Fdigit radix (Fopp x) = Fdigit radix x.
proof: Proof. intros x; unfold Fopp, Fdigit in |- *; simpl in |- *. rewrite <- (digit_abs radix (- Fnum x)). rewrite <- (digit_abs radix (Fnum x)). case (Fnum x); simpl in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz