proposition: Lemma trans_succ : transitive succ.
proof: Proof. apply Rof_trans. unfold succ_vec. intros v1 v2 v3 h12 h23. intuition. trans v2; hyp. apply gt_trans with (vec_at0 v2); hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil BigNUtil AMatrixBasedInt)