proposition: Lemma natsUpTo_correct: forall n m, nat_depth m <= n <-> List.In m (natsUpTo n).
proof: Proof. induction n; intros; unfold nat_depth in *; split; intros; simpl in *. - exfalso. lia. - contradiction. - assert (n = m \/ S m <= n) as C by lia. destruct C as [C | C]; firstorder idtac. - destruct H. + lia. + specialize (IHn m). apply proj2 in IHn. specialize (IHn H). lia. Qed.
imports: Arith Lia List