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