proposition: Lemma psv_distrib_left : forall dim c1 c2 (r:vector dim), prod_scal_vec _ (plus c1 c2) r ==v sum_vector _ (prod_scal_vec dim c1 r) (prod_scal_vec _ c2 r).
proof: Proof. fix psv_distrib_left 1. intros [|dim]. simpl. intros. apply mult_distrib_left. simpl vector. intros c1 c2 [a r]. simpl. split. apply mult_distrib_left. apply psv_distrib_left. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)