proposition: Lemma Vfold_left_rev_gtx_compat : forall n (v v' : vector A n), (forall i (ip: i < n), Vnth v ip >_0 Vnth v' ip) -> Vfold_left_rev Aplus A0 v >_0 Vfold_left_rev Aplus A0 v'.
proof: Proof. induction v; simpl; intros. VOtac. simpl. right. intuition. VSntac v'. simpl. apply gtx_plus_compat. apply IHv. intros. apply Vforall2_elim_nth. change v with (Vtail (Vcons h v)). apply Vforall2_tail. apply Vforall2_intro_nth. hyp. change h with (Vhead (Vcons h v)). rewrite !Vhead_nth. apply (H _ (PeanoNat.Nat.lt_0_succ n)). Qed.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)