proposition: Lemma lt_wf_double_ind : forall P:nat -> nat -> Prop, (forall n m, (forall p (q:nat), p < n -> P p q) -> (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
proof: Proof. intros P Hrec p. pattern p. apply lt_wf_ind. intros n H q. pattern q. apply lt_wf_ind. auto. Defined.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts)