proposition: Lemma map_seqZ_disjoint start1 start2 xs1 xs2 : map_seqZ (M:=M A) start1 xs1 ##ₘ map_seqZ (M:=M A) start2 xs2 ↔ start1 + Z.of_nat (length xs1) ≤ start2 ∨ start2 + Z.of_nat (length xs2) ≤ start1 ∨ length xs1 = 0%nat ∨ length xs2 = 0%nat.
proof: Proof. rewrite map_disjoint_alt. setoid_rewrite lookup_map_seqZ_None. split; intros Hi; [|lia]. pose proof (Hi start1). pose proof (Hi start2). lia. Qed.
imports: Coq(Permutation) stdpp(options)