proposition: Theorem Babs_idempotent : forall (x: binary_float), Babs (Babs x) = Babs x.
proof: Proof. now intros [sx|sx| |sx mx ex Hx]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative