proposition: Lemma vec_plus_ge_compat_l : forall n (vl vr vr' : vec n), vr >=v vr' -> vl [+] vr >=v vl [+] vr'.
proof: Proof. intros. apply vec_plus_ge_compat. refl. hyp. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)