proposition: Lemma prc_distrib_left : forall dim c1 c2 (r:vector dim), prod_row_col _ (sum_vector _ c1 c2) r == plus (prod_row_col dim c1 r) (prod_row_col _ c2 r).
proof: Proof. apply prc_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)