fact: Definition measure2 A1 A2 (f : A1 -> A2 -> nat) : binary (A1*A2) := fun p1 p2 => let (x1,y1) := p1 in let (x2,y2) := p2 in (f x1 y1 < f x2 y2).
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)