proposition: Lemma succ_wf : WF succ.
proof: Proof. apply wf_transp_WF. unfold succ, transp. apply well_founded_lt_compat with (f := (fun d: dom => match vec_at0 (dom2vec d) with | Fin x => Z.abs_nat x | MinusInfBZ => 0%nat end ) ). intros x y xy. destruct x. destruct y. simpl. cut (ge (vec_at0 x) A1). 2: hyp. cut (ge (vec_at0 x0) A1). 2: hyp. cut (gtx (vec_at0 x0) (vec_at0 x)). gen (vec_at0 x0). gen (vec_at0 x). clear x x0 v v0 xy. intros x y xy x_lb y_lb. destruct x; destruct y; arctic_ord. unfold A1, OSR.SR.A1 in *. assert ((z >= 0)%Z). apply fin_ge_impl_ge; hyp. assert ((z0 >= 0)%Z). apply fin_ge_impl_ge; hyp. destruct xy. simpl in H1. apply Zabs_nat_lt. lia. destruct H1; discr. destruct x_lb; [ contr | discr ]. destruct y_lb; [ contr | discr ]. destruct y_lb; [ contr | discr ]. unfold vec_at0. apply Vforall2_elim_nth. hyp. Qed.
imports: Coq(ZArith Lia) CoLoR(LogicUtil Matrix AMonAlg AArcticBasedInt VecUtil OrdSemiRing SN RelUtil AMatrixBasedInt ListUtil)