proposition: Lemma mat_eq : forall m n (M N : matrix m n), (forall i j (ip : i < m) (jp : j < n), get_elem M ip jp = get_elem N ip jp) -> M = N.
proof: Proof. unfold matrix. induction m; simpl; intros. VOtac. refl. unfold get_elem, get_row in H. VSntac M. VSntac N. apply Vcons_eq_intro. apply Veq_nth. intros. rewrite !Vhead_nth. apply H. apply IHm. intros. unfold get_elem, get_row. rewrite !Vnth_tail. apply H. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)