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:Xnat) (g:Ynat) x y p IH
  := well_founded_induction_type_2 p (lex_size_lt_wf f g) IH x y.