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