proposition: Lemma GoM_SCC : forall x y, GoM (SCC_mat M) x y <-> SCC (GoM M) x y.
proof: Proof. unfold SCC_mat in *; split; intros; rewrite Gmorph_intersect in *; try rewrite Gmorph_transpose in *; unfold transp in *; rewrite !Gmorph_clos_trans in *; unfold SCC in *; trivial. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)