proposition: Lemma transp_mat_unbound : forall x y, M[[x,y]] = (mat_transpose M)[[y,x]].
proof: Proof. intros; unfold mat_unbound. destruct (le_gt_dec dim x); auto; destruct (le_gt_dec dim y); auto. unfold mat_transpose; rewrite mat_build_nth; trivial. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)