proposition: Lemma surjective_injective_antisym `{AL+TOP ≪ l} {n m} {p q: X n m} {Hp: is_surjective p} {Hq: is_injective q}: p ≦ q -> p ≡ q.
proof: Proof. intros Hpq. cnv_switch. apply univalent_antisym. cnv_switch; ra_normalise. rewrite surjective_tx. lattice. now cnv_switch. Qed.
imports: common lattice monoid kleene normalisation rewriting