fact: Definition lexico2 {A1 A2} (R1:binary A1) (R2:binary A2) : binary (A1*A2) := fun p1 p2 : A1*A2 => let (x1,x2) := p1 in let (y1,y2) := p2 in (R1 x1 y1) \/ (x1 = y1) /\ (R2 x2 y2).
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)