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