proposition: Lemma invset_join s t : invset (s \/R t) = tclosure (invset s :|: invset t).
proof: Proof. by rewrite /Order.join invset_supperm. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype