proposition: Lemma mat_transpose_row_col : forall m n (M : matrix m n) i (ip : i < m), get_col (mat_transpose M) ip = get_row M ip.
proof: Proof. intros. apply Veq_nth. intros. mat_get_simpl. unfold mat_transpose. rewrite mat_build_nth. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)