proposition: Theorem Fplus_same_exp : forall m1 m2 e, Fplus (Float m1 e) (Float m2 e) = Float (m1 + m2) e.
proof: Proof. intros m1 m2 e. unfold Fplus. simpl. now rewrite Zle_bool_refl, Zminus_diag, Zmult_1_r. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop