proposition: Lemma MODULE_comp : forall (a b : R) (x y : Mod), Equal a b -> Equal x y -> Equal (module_mult a x) (module_mult b y).
proof: Proof. intros a b x y H' H'0; try assumption. apply Trans with (module_mult a y); unfold module_mult in |- *. apply Ap_comp; auto with algebra. apply Ap_comp; auto with algebra. Qed.
imports: Module_cat Abelian_group_facts