proposition: Theorem sub_fils : forall a b c : R, forall zi : FF, BND (-(b - c)) zi -> BND ((a - b) - (a - c)) zi.
proof: Proof. intros a b c zi Hz. replace ((a - b) - (a - c))%R with (-(b - c))%R. exact Hz. ring. Qed.
imports: Reals Gappa_common