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. apply pcr_prc_comm with (eq:=eq) (plus:=plus) (mult:=mult). apply eq_Equivalence. intros;ring. intros;ring. intros;ring. intros;ring. apply plus_morph. apply mult_morph. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)