proposition: Lemma existandb_matmult : forall x y, (M <*> N)[[x, y]] = true <-> exists z, M[[x,z]] && N[[z,y]] = true.
proof: Proof. intros. unfold mat_unbound. destruct (le_gt_dec dim x). simpl; intuition. destruct H; tauto. destruct (le_gt_dec dim y). intuition. destruct H. destruct (le_gt_dec dim x0). trivial. destruct H; sym; apply andb_false_r. unfold mat_mult; rewrite mat_build_nth; unfold get_row; unfold get_col. split; intros. rewrite existandb_dotprod in H; repeat destruct H; exists x0. destruct (le_gt_dec dim x0); auto with *. apply Is_true_eq_true; unfold gt in g1; gen (lt_unique x1 g1); intro; subst. rewrite Vnth_map in H; auto. destruct H; destruct (le_gt_dec dim x0). simpl in *; discr. rewrite existandb_dotprod. exists x0; exists g1; rewrite Vnth_map; auto with *. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)