proposition: Lemma pmc_distrib_right : forall dim m (c1 c2:vector dim), prod_mat_col _ m (sum_vector _ c1 c2) ==v sum_vector _ (prod_mat_col dim m c1) (prod_mat_col _ m c2).
proof: Proof. apply pmc_distrib_right with (eq:=eq) (plus:=plus) (mult:=mult). apply eq_Equivalence. intros;ring. intros;ring. intros;ring. intros;ring. apply plus_morph. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)