proposition: Lemma orb_matadd : forall x y, (M <+> N)[[x, y]] = M[[x, y]] || N[[x, y]].
proof: Proof. intros. unfold mat_unbound. destruct (le_gt_dec dim x); auto. destruct (le_gt_dec dim y); auto. unfold mat_plus. unfold vec_plus. mat_get_simpl. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)