proposition: Lemma vec_plus_gt_compat_r : forall vl vl' vr vr', vec_at0 vl > vec_at0 vl' -> vec_at0 vr >= vec_at0 vr' -> vec_at0 (vl [+] vr) > vec_at0 (vl' [+] vr').
proof: Proof. unfold MBI.vec_at0, vector_plus. intros. simpl. rewrite !Vnth_map2. unfold Aplus, Peano.gt. apply plus_gt_compat_l; hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)