proposition: Theorem add_filq : forall a b c : R, forall zi : FF, NZR (a + c) -> BND ((b - c) / (a + c)) zi -> BND (((a + b) - (a + c)) / (a + c)) zi.
proof: Proof. intros a b c zi Hac Hz. replace (((a + b) - (a + c)) / (a + c))%R with ((b - c) / (a + c))%R. exact Hz. field. exact Hac. Qed.
imports: Reals Gappa_common