proposition: Lemma pcr_prc_comm : forall dim c1 r c2, prod_mat_col dim (prod_col_row _ c1 r) c2 ==v prod_scal_vec _ (prod_row_col _ r c2) c1.
proof: Proof. fix pcr_prc_comm 1. intros [|dim]. intros;simpl. rewrite (mult_comm c1). do 2 rewrite mult_assoc. rewrite (mult_comm c1). reflexivity. simpl; intros [a1 c1] [a2 r2] [a3 r3]. constructor. 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. rewrite (mult_comm a1). do 2 rewrite mult_assoc. rewrite (mult_comm a1). rewrite prc_comm_sv_left. rewrite (mult_comm a1). reflexivity. rewrite psv_assoc. rewrite pcr_prc_comm. rewrite psv_distrib_left. rewrite mult_comm. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)