proposition: Lemma succ_wf : WF succ.
proof: Proof. apply WF_incl with (fun x y => vec_at0 (dom2vec x) >> vec_at0 (dom2vec y)). intros x y xy. destruct (@Vforall2_elim_nth _ _ gtx _ (dom2vec x) (dom2vec y) _ dim_pos xy). hyp. destruct H. destruct x. absurd (Vnth x dim_pos = A0). apply ge_A1_not_minusInf. hyp. hyp. fold (@Rof dom A gt (fun v => vec_at0 (dom2vec v))). apply WF_inverse. apply gt_WF. Qed.
imports: CoLoR(AArcticBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil)