proposition: Lemma rewrite_gt : forall x xi n, BND x xi -> rewrite_gt_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. unfold Rgt. apply Rlt_le_trans with (2 := proj1 Hx). exact H. Qed.
imports: Flocq.Core.Defs Gappa_common Gappa_pred_bnd