proposition: Lemma join_1: forall n N1 N2, In n N1 -> In n (join N1 N2).
proof: Proof. unfold In, join; intros; cbn. split; apply Zinf.max_1; tauto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)