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. apply prm_pmc_comm with (eq:=eq) (plus:=plus) (mult:=mult). apply eq_Equivalence. intros;ring. intros;ring. 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)