proposition: Lemma rewrite_le0 : forall x : R, forall xi : FF, BND x xi -> rewrite_le0_helper xi = true -> (x <= 0)%R.
proof: Proof. intros x xi Hx Hb. generalize (Fneg0_correct _ Hb). clear Hb. intro H. apply Rle_trans with (1 := proj2 Hx). exact H. Qed.
imports: Flocq.Core.Defs Gappa_common Gappa_pred_bnd