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