proposition: Lemma nat_complete_double_ind : forall P : nat -> nat -> Prop, (forall m n, (forall m' n', m' < m -> n' < n -> P m' n') -> P m n) -> forall m n, P m n.
proof: Proof. intros P H m. pattern m in |- *; apply lt_wf_ind; auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)