proposition: Lemma im_neutral_pmc : forall dim c, prod_mat_col _ (id_matrix dim) c ==v c.
proof: Proof. induction dim. simpl;intros;ring. simpl. unfold null_vector;intros [a v]. split. rewrite nv_nullify_prc_left. ring. rewrite nv_nullify_psv. rewrite nv_neutral_left_sv. rewrite IHdim. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)