proposition: Lemma GoM_true_bounds : forall x y, GoM M x y -> x < dim /\ y < dim.
proof: Proof. intros. split; unfold GoM, mat_unbound in H; destruct (le_gt_dec dim x); destruct (le_gt_dec dim y); try discr; auto with *. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)