proposition: Theorem lexico_wf: well_founded lexico.
proof: Proof. intros [a b]. revert b. induction a as [a IHa] using (well_founded_induction HR). induction b as [b IHb] using (well_founded_induction HS). constructor. intros [a' b'] H. inversion_clear H; auto. Qed.
imports: ATBR(Common)