proposition: Lemma ALGEBRA_comp : forall x x' y y' : A, Equal x x' -> Equal y y' -> Equal (algebra_mult x y) (algebra_mult x' y').
proof: Proof. intros x x' y y' H' H'0; try assumption. unfold algebra_mult in |- *. apply Ap_comp. auto with algebra. apply (Ap_comp (B:=Hom_module (algebra_carrier A) (algebra_carrier A)) (f:=algebra_bilinear_map (algebra_on_def A)) (g:=algebra_bilinear_map (algebra_on_def A)) H'). auto with algebra. Qed.
imports: Algebra Ring_util