proposition: Lemma rewrite_ge : forall x xi n, BND x xi -> rewrite_ge_helper xi n = true -> (x >= Float1 n)%R.
proof: Proof. intros x xi n Hx Hb. rewrite <- (Rmult_1_r (Float1 n)). generalize (Fle2_correct _ _ Hb). clear Hb. intro H. apply Rle_ge. apply Rle_trans with (2 := proj1 Hx). exact H. Qed.
imports: Flocq.Core.Defs Gappa_common Gappa_pred_bnd