proposition: Lemma pm_assoc_pmc : forall dim m1 m2 c, prod_mat_col dim m1 (prod_mat_col _ m2 c) ==v prod_mat_col _ (prod_matrix _ m1 m2) c.
proof: Proof. fix pm_assoc_pmc 1. intros [|dim]. intros;simpl. symmetry;apply mult_assoc. simpl; intros [a1 [r1 [c1 m1]]] [a2 [r2 [l2 m2]]] [a3 c3]. f_equal. repeat rewrite mult_distrib_right. repeat rewrite prc_distrib_right. repeat rewrite prc_comm_sv_right. repeat rewrite mult_distrib_right. repeat rewrite mult_distrib_left. repeat rewrite plus_assoc. constructor. rewrite <- mult_assoc. rewrite <- (plus_assoc (mult a1 (prod_row_col dim r2 c3))). rewrite (plus_comm (mult a1 (prod_row_col dim r2 c3))). rewrite plus_assoc . match goal with |- plus _ ?t == plus _ ?t' => assert (Heq: t == t');[|rewrite Heq;reflexivity] end. rewrite mult_comm. match goal with |- plus _ ?t == plus _ ?t' => assert (Heq: t == t');[|rewrite Heq;reflexivity] end. rewrite prc_distrib_left. rewrite prc_comm_sv_left. rewrite prm_pmc_comm. reflexivity. repeat rewrite psv_distrib_right. repeat rewrite psv_assoc. repeat rewrite pmc_distrib_left. repeat rewrite pmc_distrib_right. repeat rewrite psv_distrib_left. repeat rewrite sum_vector_assoc. match goal with |- sum_vector _ ?a ?b ==v sum_vector _ ?a' ?b' => assert (Heq1: a ==v a');[| assert (Heq2: b ==v b');[|rewrite Heq1;rewrite Heq2;reflexivity] ] end. rewrite mult_comm. reflexivity. rewrite pcr_prc_comm. rewrite <- sum_vector_assoc. rewrite (sum_vector_comm _ (prod_scal_vec dim (prod_row_col dim r2 c3) c1)). rewrite sum_vector_assoc. rewrite pmc_comm_sv_right. rewrite pm_assoc_pmc. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)