proposition: Lemma GoM_restricted : is_restricted (GoM M) (nats_decr_lt dim).
proof: Proof. unfold is_restricted; intros x y. rewrite <- !In_nats_decr_lt. intro. unfold GoM in H. unfold mat_unbound in *. destruct (le_gt_dec dim x); auto. discr. destruct (le_gt_dec dim y); auto. discr. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)