proposition: Lemma prc_distrib_right : forall dim c (r1 r2:vector dim), prod_row_col _ c (sum_vector _ r1 r2) == plus (prod_row_col dim c r1) (prod_row_col _ c r2).
proof: Proof. apply prc_distrib_right 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)