LeftHeteroDistribute vector_lact vector_plus vector_plus. Proof. intros r v1 v2; apply path_vector; intros i Hi. rewrite 5 entry_Build_Vector. apply distribute_l. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.PathGroupoids. Require Import Types.Sigma. Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring Algebra.Rings.Module. Require Import Spaces.Nat.Core. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import abstract_algebra.