proposition: Lemma is_nan_neg x : F.is_nan (F.neg x) = F.is_nan x.
proof: Proof. rewrite !F.is_nan_correct. generalize (F.neg_correct x). case_eq (F.classify x); [|now intros _ H; rewrite H..]. intro Hx. generalize (F.classify_correct x); rewrite Hx, F.real_correct. case F.toX; [easy|]; intros rx _. generalize (F.classify_correct (F.neg x)). rewrite F.real_correct. case F.toX; [easy|]; intros rnx. now case F.classify. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic