proposition: Theorem is_Fzero_rep2 : forall x : float, x = 0%R :>R -> is_Fzero x.
proof: Proof. intros x H'. case (Rmult_integral _ _ H'); simpl in |- *; auto. case x; simpl in |- *. intros Fnum1 Fexp1 H'0; red in |- *; simpl in |- *; auto with real zarith. apply eq_IZR_R0; auto. intros H'0; contradict H'0; apply powerRZ_NOR. now apply Rgt_not_eq, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz