proposition: Theorem abs_of_uabs : forall x : R, forall zi : FF, BND (Rabs x) zi -> Fpos0 (lower zi) = true -> ABS x zi.
proof: Proof. intros x zi Hx Hb. generalize (Fpos0_correct _ Hb). clear Hb. intro H1. exact (conj H1 Hx). Qed.
imports: Gappa_common Gappa_pred_nzr