proposition: Lemma GoM_MoG : forall x y, GoM MoG x y <-> R x y.
proof: Proof. intros. unfold GoM, mat_unbound. split; intros; destruct (le_gt_dec dim x); destruct (le_gt_dec dim y); try ded (hyp H); auto; intuition; try lia; try tauto; try discr. unfold MoG in H; rewrite mat_build_nth in H. destruct (R_dec x y); auto; try discr. unfold MoG; rewrite mat_build_nth. destruct (R_dec x y); auto with *. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)