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. apply pm_assoc_pmc 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)