proposition: Lemma prm_pmc_comm : forall dim r m c, prod_row_col dim (prod_row_mat _ r m) c == prod_row_col dim r (prod_mat_col _ m c).
proof: Proof. fix prm_pmc_comm 1. intros [|dim]. simpl;intros;apply mult_assoc. simpl; intros [a1 r1] [a2 [r2 [c2 m2]]] [a3 c3]. repeat rewrite mult_distrib_right. repeat rewrite mult_distrib_left. repeat rewrite prc_distrib_right. repeat rewrite prc_distrib_left. repeat rewrite plus_assoc. rewrite mult_assoc. assert ( Heq: (plus (mult (prod_row_col dim r1 c2) a3) (plus (prod_row_col dim (prod_scal_vec dim a1 r2) c3) (prod_row_col dim (prod_row_mat dim r1 m2) c3))) == (plus (mult a1 (prod_row_col dim r2 c3)) (plus (prod_row_col dim r1 (prod_scal_vec dim a3 c2)) (prod_row_col dim r1 (prod_mat_col dim m2 c3))))); [|rewrite Heq;reflexivity]. rewrite <- plus_assoc. rewrite (plus_comm (mult (prod_row_col dim r1 c2) a3)). rewrite plus_assoc. rewrite prc_comm_sv_left. assert (Heq:(plus (mult (prod_row_col dim r1 c2) a3) (prod_row_col dim (prod_row_mat dim r1 m2) c3))== (plus (prod_row_col dim r1 (prod_scal_vec dim a3 c2)) (prod_row_col dim r1 (prod_mat_col dim m2 c3)))); [|rewrite Heq;reflexivity]. rewrite prc_comm_sv_right. rewrite mult_comm. rewrite prm_pmc_comm. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)