proposition: Lemma mat_transpose_col_row : forall m n (M : matrix m n) i (ip : i < n), get_row (mat_transpose M) ip = get_col 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)