proposition: Lemma lex_nat_wf : well_founded lex_nat.
proof: Proof. intros (a, b); pattern a, b; apply lt_wf_double_ind. intros m n H1 H2. constructor; intros (m', n') [G | [-> G]]. - now apply H1. - now apply H2. Defined.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts)