proposition: Theorem erase_correct : forall x, erase x = x.
proof: Proof. destruct x as [s|s|s pl H|s m e H] ; try easy ; simpl. - apply f_equal, eqbool_irrelevance. - apply f_equal, eqbool_irrelevance. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN