proposition: Theorem canonical_opp : forall m e, canonical (Float beta m e) -> canonical (Float beta (-m) e).
proof: Proof. intros m e H. unfold canonical. now rewrite F2R_Zopp, cexp_opp. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop