proposition: Lemma prc_distrib_right : forall dim c (r1 r2:vector dim), prod_row_col _ c (sum_vector _ r1 r2) == plus (prod_row_col dim c r1) (prod_row_col _ c r2).
proof: Proof. fix prc_distrib_right 1. intros [|dim]. simpl. intros. apply mult_distrib_right. simpl vector. intros [a1 c1] [a2 c2] [a r]. simpl. rewrite prc_distrib_right. repeat rewrite mult_distrib_right. repeat rewrite plus_assoc. rewrite <- (plus_assoc (prod_row_col dim c1 c2) (mult a1 a) ) . rewrite (plus_comm (prod_row_col dim c1 c2) (mult a1 a) ) . repeat rewrite plus_assoc. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)