proposition: Lemma nm_neutral_left_sum_matrix : forall dim v, sum_matrix dim (null_matrix dim) v ==m v.
proof: Proof. induction dim. simpl. unfold null_matrix. simpl. intros;ring. simpl. intros [a [r [c m]]]. repeat split;try ring. apply nv_neutral_left_sv. apply nv_neutral_left_sv. apply IHdim. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)