proposition: Lemma Bsign_pos x r : BtoX x = Xreal r -> (0 < r)%R -> Bsign x = false.
proof: Proof. intros H H'; revert H. case x as [s|s| |s m e B]; [ |now simpl..| ]. { case s; simpl; [ |now simpl]. intro H; injection H; clear H; intro H. now exfalso; apply (Rlt_irrefl 0); rewrite H at 2. } case s; simpl; [ |now simpl]. intro H; exfalso. injection H; clear H; intro H. revert H'; rewrite <- H. apply Rle_not_lt, Rlt_le, Generic_proof.FtoR_Rneg. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig