proposition: Theorem bnd_of_nzr_rel : forall a b : R, forall zi : FF, NZR b -> REL a b zi -> BND ((a - b) / b) zi.
proof: Proof. intros a b zi Hb (x,(Hr1,Hr2)). replace ((a - b) / b)%R with x. exact Hr1. rewrite Hr2. field. exact Hb. Qed.
imports: Gappa_common Gappa_pred_bnd