proposition: Theorem NisFzeroComp : forall x y : float, ~ is_Fzero x -> x = y :>R -> ~ is_Fzero y.
proof: Proof. intros x y H' H'0; contradict H'. apply is_Fzero_rep2; auto. rewrite H'0. apply is_Fzero_rep1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz