proposition: Lemma Rsgn_div : forall x y : R, x <> 0%R -> y <> 0%R -> Rlt_bool (x / y) 0 = xorb (Rlt_bool x 0) (Rlt_bool y 0).
proof: Proof. intros x y Hx0 Hy0. unfold Rdiv. case (Rlt_bool_spec x) ; intros Hx ; case (Rlt_bool_spec y) ; intros Hy. apply Rlt_bool_false. rewrite <- Rmult_opp_opp. apply Rlt_le, Rmult_lt_0_compat. now apply Ropp_gt_lt_0_contravar. apply Ropp_gt_lt_0_contravar. now apply Rinv_lt_0_compat. apply Rlt_bool_true. apply Ropp_lt_cancel. rewrite Ropp_0, <- Ropp_mult_distr_l_reverse. apply Rmult_lt_0_compat. now apply Ropp_gt_lt_0_contravar. apply Rinv_0_lt_compat. destruct Hy as [Hy|Hy]. easy. now elim Hy0. apply Rlt_bool_true. apply Ropp_lt_cancel. rewrite Ropp_0, <- Ropp_mult_distr_r_reverse. apply Rmult_lt_0_compat. destruct Hx as [Hx|Hx]. easy. now elim Hx0. apply Ropp_gt_lt_0_contravar. now apply Rinv_lt_0_compat. apply Rlt_bool_false. apply Rlt_le, Rmult_lt_0_compat. destruct Hx as [Hx|Hx]. easy. now elim Hx0. apply Rinv_0_lt_compat. destruct Hy as [Hy|Hy]. easy. now elim Hy0. Qed.
imports: Coq(ZArith Reals) Flocq(Core Bracket Round Operations Div Sqrt)