proposition: Lemma rewrite_lt : forall x xi n, BND x xi -> rewrite_lt_helper xi n = true -> (x < Float1 n)%R.
proof: Proof. intros x xi n Hx Hb. rewrite <- (Rmult_1_r (Float1 n)). generalize (Flt2_correct _ _ Hb). clear Hb. intro H. apply Rle_lt_trans with (1 := proj2 Hx). exact H. Qed.
imports: Flocq.Core.Defs Gappa_common Gappa_pred_bnd