proposition: Lemma vec_plus_gt_compat_l : 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. rewrite !Vnth_map2. unfold Aplus. apply plus_gt_compat_r; hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)