proposition: Lemma four_ind : forall P : nat -> Prop, P 0 -> P 1 -> P 2 -> P 3 -> (forall n, P n -> P (S (S (S (S n))))) -> forall n, P n.
proof: Proof. intros. apply lt_wf_ind. intro m. case m; auto. clear m; intro m. case m; auto. clear m; intro m. case m; auto. clear m; intro m. case m; auto with arith. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)