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