proposition: Theorem mul_filq : forall a b c : R, forall zi : FF, REL b c zi -> REL (a * b) (a * c) zi.
proof: Proof. intros a b c zi (ze, (Hz1, Hz2)). exists ze. split. exact Hz1. rewrite Hz2. apply sym_eq. apply Rmult_assoc. Qed.
imports: Reals Gappa_common