proposition: Lemma gt_wf_ind : forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
proof: Proof. Proof lt_wf_ind. Lemma lt_wf_double_rect : forall P:nat -> nat -> Type, (forall n m, (forall p q, p < n -> P p q) -> (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. Proof. intros P Hrec p; pattern p; apply lt_wf_rect. intros n H q; pattern q; apply lt_wf_rect; auto. Defined.
imports: PeanoNat