proposition: Theorem Fopp_Fminus_dist : forall p q : float, Fopp (Fminus p q) = Fminus (Fopp p) (Fopp q).
proof: Proof. intros p q; case p; case q; unfold Fopp, Fminus, Fplus in |- *; simpl in |- *; auto. intros; apply floatEq; simpl in |- *; repeat rewrite (Z.min_comm Fexp Fexp0); repeat rewrite Zopp_mult_distr_l_reverse; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz