proposition: Lemma tx_surjective `{AL+TOP ≪ l} n m (x: X m n): top' n n ≦ top⋅x -> is_surjective x.
proof: Proof. intro E. unfold is_surjective. transitivity (1 ∩ (top' n m ⋅ x)). rewrite <-E. lattice. rewrite capC, capxdot. ra. Qed.
imports: common lattice monoid kleene normalisation rewriting