proposition: Lemma min_correct : forall x y, match classify x, classify y with | Fnan, _ | _, Fnan => classify (min x y) = Fnan | Fminfty, _ | _, Fminfty => classify (min x y) = Fminfty | Fpinfty, _ => min x y = y | _, Fpinfty => min x y = x | Freal, Freal => toX (min x y) = Xmin (toX x) (toX y) end.
proof: Proof. intros x y. case_eq (classify x); [|now case x..]. case_eq (classify y); [|now case y; [case x; [..|intros b p z; case b]|..]|now case y..]. now rewrite (Fmin_correct radix). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig