proposition: Lemma In_mono: forall n1 n2 N, n1 <= n2 -> In n2 N -> In n1 N.
proof: Proof. unfold In; destruct N; intros. lia. auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)