proposition: Lemma G_morph_id : forall x y, GoM (id_matrix dim) x y <-> x=y /\ x<dim /\ y<dim.
proof: Proof. intros. unfold GoM. apply mat_id_spec. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)