proposition: Theorem Fabs_Fzero : forall x : float, ~ is_Fzero x -> ~ is_Fzero (Fabs x).
proof: Proof. intros x; case x; unfold is_Fzero in |- *; simpl in |- *. intros n m; case n; simpl in |- *; auto with zarith; intros; red in |- *; discriminate. Qed.
imports: Reals ZArith List PeanoNat Psatz