proposition: Theorem Fnormalize_Fopp : forall p : float, Fnormalize (Fopp p) = Fopp (Fnormalize p).
proof: Proof. intros p; case p; unfold Fnormalize in |- *; simpl in |- *. intros Fnum1 Fexp1; case (Z_zerop Fnum1); intros H'. rewrite H'; simpl in |- *; auto. case (Z_zerop (- Fnum1)); intros H'0; simpl in |- *; auto. case H'; replace Fnum1 with (- - Fnum1)%Z; auto with zarith. unfold Fopp, Fshift, Fdigit in |- *; simpl in |- *. replace (digit radix (- Fnum1)) with (digit radix Fnum1). apply floatEq; simpl in |- *; lia. case Fnum1; simpl in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz