proposition: Lemma Gmorph_plus : forall x y, GoM (M <+> N) x y <-> ((GoM M) U (GoM N)) x y.
proof: Proof. intros. assert (GoM (M <+> N) x y <-> (GoM M x y \/ GoM N x y)). unfold GoM. rewrite orb_matadd. split; intro. eapply orb_prop; auto. destruct H; auto with *. auto. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)