proposition: Lemma trans_measure : forall (f : A -> nat), trans (measure f).
proof: Proof. Proof using. intros. unfold measure, trans. intros. nat_math. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)