proposition: Lemma Fis0_correct : forall x : float2, Fis0 x = true -> x = 0%R :>R.
proof: Proof. intros x. unfold Fis0. induction x. induction Fnum ; intro H0 ; try discriminate. apply float2_zero. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions