proposition: Lemma ltB_wf : well_founded lt.
proof: Proof. intro b. apply Acc_intro. fo. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec) CoLoR(VecUtil) CoLoR(LCompRewrite) CoLoR(SN LCall) CoLoR(EqUtil) CoLoR(LCompInt)