proposition: Lemma andb_mat_unbound : forall x y, (mat_andb M N)[[x,y]] = M[[x,y]] && N[[x,y]].
proof: Proof. intros; unfold mat_unbound. destruct (le_gt_dec dim x); auto with *. destruct (le_gt_dec dim y); auto with *. unfold mat_andb; rewrite !Vnth_map2; auto. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)