proposition: Lemma mat_id_spec : forall x y, (id_matrix dim)[[x,y]] = true <-> x=y /\ x<dim /\ y<dim.
proof: Proof. intros. split; intro. unfold mat_unbound in H. destruct (le_gt_dec dim x). discr. destruct (le_gt_dec dim y). discr. unfold id_matrix in H; rewrite Vbuild_nth in H. destruct (eq_nat_dec x y). auto. unfold id_vec, zero_vec in H. rewrite Vnth_replace_neq in H. rewrite Vnth_const in H. discr. hyp. destruct H; destruct H0; unfold mat_unbound. destruct (le_gt_dec dim x); auto with *. destruct (le_gt_dec dim y); auto with *. unfold id_matrix; rewrite Vbuild_nth. unfold id_vec. subst x. replace g0 with g. apply Vnth_replace. apply lt_unique. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)