proposition: Lemma prm_distrib_left : forall dim r1 r2 (m:matrix dim), prod_row_mat _ (sum_vector _ r1 r2) m ==v sum_vector _ (prod_row_mat dim r1 m) (prod_row_mat _ r2 m).
proof: Proof. apply prm_distrib_left with (eq:=eq) (plus:=plus) (mult:=mult). apply eq_Equivalence. 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)