proposition: Lemma wf_nat_upto : forall (b:nat), wf (nat_upto b).
proof: Proof. Proof using. intros b n. induction_wf IH: (wf_measure (fun n => (b-n)%nat)) n. apply Acc_intro. introv [H1 H2]. apply IH. hnf. nat_math. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)