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