proposition: Theorem sub_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