Library LexSizeInduction

Require Import Base Recdef.

Lexiographic Size Induction

Induction on the lexeographoic ordering un tuples with size function

Definition lex_size_lt X Y f g (p1 p2 : X ×Y) :=
  let (x1,y1) := p1 in
  let (x2,y2) := p2 in
  f x1 = f x2 ∧ g y1 < g y2 ∨ f x1 < f x2.

Lemma lex_size_lt_wf X Y (f : X → nat) (g:Y → nat): well_founded (lex_size_lt f g).

Definition lex_size_induction X Y (f:X →nat) (g:Y →nat) x y p IH
  := well_founded_induction_type_2 p (lex_size_lt_wf f g) IH x y.