proposition: Lemma mat_transpose_idem : forall m n (M : matrix m n), mat_transpose (mat_transpose M) = M.
proof: Proof. intros. apply mat_eq . intros. unfold mat_transpose. rewrite !mat_build_elem. refl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)