proposition: Lemma wf_upto : forall n, wf (upto n).
proof: Proof. Proof using. intros b n. induction_wf IH: (wf_measure (fun n => Z.abs_nat (b-n))) n. apply Acc_intro. introv [H1 H2]. apply IH. applys lt_abs_abs; math. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)