proposition: Lemma measure_induction : forall (A:Type) (mu:A->nat) (P:A->Prop), (forall x, (forall y, mu y < mu x -> P y) -> P x) -> (forall x, P x).
proof: Proof. Proof using. introv IH. intros x. gen_eq n: (mu x). gen x. induction n using peano_induction. introv Eq. subst*. Qed.
imports: Coq.Arith.Arith Coq.micromega.Lia TLC(LibTactics LibReflect LibBool LibOperation LibRelation LibOrder)