proposition: Lemma succ_wf : WF succ.
proof: Proof. apply WF_incl with (Rof gt (fun v : dom => vec_at0 (dom2vec v))). unfold succ, succ_vec, Rof, gt. intros x y. intuition. apply WF_inverse. apply gt_WF. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)