proposition: Lemma add_1: forall n1 n2 N1 N2, In n1 N1 -> In n2 N2 -> In (n1 + n2) (add N1 N2).
proof: Proof. unfold add; intros. destruct (isempty N1) eqn:E1. elim (isempty_1 n1 N1); auto. destruct (isempty N2) eqn:E2. elim (isempty_1 n2 N2); auto. destruct H; destruct H0; split; cbn. apply Zinf.add_1; auto. replace (- (n1 + n2)) with ((-n1) + (-n2)) by lia. apply Zinf.add_1; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)