proposition: Theorem Req_bool_spec : forall x y, Req_bool_prop x y (Req_bool x y).
proof: Proof. intros x y. unfold Req_bool. case Rcompare_spec ; constructor. now apply Rlt_not_eq. easy. now apply Rgt_not_eq. Qed.
imports: Coq(Psatz Reals ZArith) Zaux