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