proposition: Lemma Gmorph_mult : forall x y, GoM (M <*> N) x y <-> (GoM M @ GoM N) x y.
proof: Proof. intros. unfold GoM; unfold compose. rewrite existandb_matmult. intuition; destruct H as [z]; exists z; auto with *. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)