proposition: Lemma lang_dot_leq n m p: Proper (leq ==> leq ==> leq) (lang_dot n m p).
proof: Proof. intros x y H x' y' H' w [u Hu [v Hv Hw]]. exists u. apply H, Hu. exists v. apply H', Hv. assumption. Qed.
imports: List prop monoid