proposition: Theorem Req_bool_false : forall x y, (x <> y)%R -> Req_bool x y = false.
proof: Proof. intros x y Hxy. case Req_bool_spec ; intros H. contradict Hxy. exact H. apply refl_equal. Qed.
imports: Coq(Psatz Reals ZArith) Zaux