proposition: Theorem Rlt_bool_cond_Ropp : forall x sx, (0 < x)%R -> Rlt_bool (cond_Ropp sx x) 0 = sx.
proof: Proof. intros x sx Hx. destruct sx; simpl. - apply Rlt_bool_true. now apply Ropp_lt_gt_0_contravar. - apply Rlt_bool_false. now left. Qed.
imports: Coq(Psatz Reals ZArith) Zaux