proposition: Lemma in_count: forall m n, n < m -> List.In n (count m).
proof: Proof. induction m; intros. { inversion H. } inversion H; subst; clear H. { simpl. auto. } simpl. right. auto. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List