proposition: Theorem Fexp_Fplus : forall f1 f2 : float beta, Fexp (Fplus f1 f2) = Z.min (Fexp f1) (Fexp f2).
proof: Proof. intros f1 f2. unfold Fplus. rewrite <- Falign_spec_exp. now destruct (Falign f1 f2) as ((p,q),e). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop