proposition: Lemma rewrite_lt0 : forall x : R, forall xi : FF, BND x xi -> rewrite_lt0_helper xi = true -> (x < 0)%R.
proof: Proof. intros x xi Hx Hb. generalize (Fneg_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