proposition: Lemma rewrite_ne : forall x xi n, BND x xi -> rewrite_ne_helper xi n = true -> (x <> Float1 n)%R.
proof: Proof. intros x xi n Hx Hb. rewrite <- (Rmult_1_r (Float1 n)). change (x <> F2R (Float radix2 n 0)). unfold Float1. destruct (orb_prop _ _ Hb) as [H|H] ; clear Hb. generalize (Flt2_correct _ _ H). clear H. intro H. apply Rlt_not_eq. apply Rle_lt_trans with (1 := proj2 Hx). exact H. generalize (Flt2_correct _ _ H). clear H. intro H. apply Rgt_not_eq. unfold Rgt. apply Rlt_le_trans with (2 := proj1 Hx). exact H. Qed.
imports: Flocq.Core.Defs Gappa_common Gappa_pred_bnd