proposition: Lemma Gmorph_transpose : forall x y, GoM (mat_transpose M) x y <-> transp (GoM M) x y.
proof: Proof. intros; unfold GoM; unfold transp; rewrite transp_mat_unbound; tauto. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)