proposition: Lemma FtoR_non_neg : forall beta s m e, (FtoR beta s m e <> 0)%R.
proof: Proof. intros beta [ | ] m e. { generalize (FtoR_Rneg beta m e); lra. } generalize (FtoR_Rpos beta m e); lra. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic