proposition: Lemma abs_correct : forall x, toX (abs x) = Xabs (toX x) /\ (valid_ub (abs x) = true).
proof: Proof. now intro x; rewrite (Fabs_correct radix). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig