proposition: Lemma vec_plus_ge_compat : forall n (vl vl' vr vr' : vec n), vl >=v vl' -> vr >=v vr' -> vl [+] vr >=v vl' [+] vr'.
proof: Proof. unfold vector_plus. intros. apply Vforall2_intro_nth. intros. simpl. rewrite !Vnth_map2. apply plus_ge_compat. apply Vforall2_elim_nth. hyp. apply Vforall2_elim_nth. hyp. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)