proposition: Theorem Cnat_double_ind : forall R : nat -> nat -> CProp, (forall n : nat, R 0 n) -> (forall n : nat, R (S n) 0) -> (forall n m : nat, R n m -> R (S n) (S m)) -> forall n m : nat, R n m.
proof: Proof. simple induction n; auto. simple induction m; auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)