Require Import Base Recdef.

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).
Proof.
  intros [x y].
  revert y. apply size_induction with (x:=x) (f:=f);clear x;intros x IHx y.
  remember x as x' eqn:eq. rewrite eq in IHx. assert (eq':f x = f x') by congruence. clear eq. revert x' eq'.
  apply size_induction with (x:=y) (f:=g);clear y;intros y IHy ? ?.
  constructor. intros [X' k'] [[eq le]|leq].
  -apply IHy;omega.
  -apply IHx;omega.
Qed.

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.

Arguments lex_size_induction {X} {Y} f g x y p IH.