proposition: Lemma map_compose_mono m1 m2 n1 n2 : m1 ⊆ m2 → n1 ⊆ n2 → m1 ∘ₘ n1 ⊆ m2 ∘ₘ n2.
proof: Proof. intros. transitivity (m1 ∘ₘ n2); [by apply map_compose_mono_l|by apply map_compose_mono_r]. Qed.
imports: Coq(Permutation) stdpp(options)