proposition: Lemma classify_correct : forall f, real f = match classify f with Freal => true | _ => false end.
proof: Proof. now intro f; case f. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig