proposition: Lemma pred_1: forall n N, In n N -> In (n - 1) (pred N).
proof: Proof. unfold pred, In; intros; destruct N; auto. lia. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)