proposition: Lemma surjective_tx `{TOP ≪ l} {n m} {x: X n m} {Hx: is_surjective x} p: top' p _ ⋅ x ≡ top.
proof: Proof. apply leq_tx_iff. transitivity (top' p _ ⋅ (x° ⋅ x)). rewrite <-surjective. ra. rewrite dotA. apply dot_leq; lattice. Qed.
imports: common lattice monoid kleene normalisation rewriting