proposition: Lemma psv_distrib_right : forall dim c (r1 r2:vector dim), prod_scal_vec _ c (sum_vector _ r1 r2) ==v sum_vector _ (prod_scal_vec dim c r1) (prod_scal_vec _ c r2).
proof: Proof. fix psv_distrib_right 1. intros [|dim]. simpl. intros. apply mult_distrib_right. simpl vector. intros c1 [a1 r1] [a2 r2]. simpl. split. apply mult_distrib_right. apply psv_distrib_right. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)