proposition: Theorem rel_of_nzr_bnd : forall a b : R, forall zi : FF, NZR b -> BND ((a - b) / b) zi -> REL a b zi.
proof: Proof. intros a b zi Hb Hr. exists ((a - b) / b)%R. split. exact Hr. now field. Qed.
imports: Gappa_common Gappa_pred_bnd