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