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