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