RightHeteroDistribute vector_lact (+) vector_plus. Proof. intros r1 r2 v; apply path_vector; intros i Hi. rewrite 4 entry_Build_Vector. apply distribute_r. 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.