proposition: Lemma vec_gt_dec : rel_dec vec_gt.
proof: Proof. unfold vec_gt, rel_dec. apply Vforall2_dec. exact gtx_dec. Defined.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)