proposition: Lemma is_invset_tclosureU A B : is_invset A -> is_invset B -> is_invset (tclosure (A :|: B)).
proof: Proof. move=> isA isB. have : A :|: B \subset Delta. by rewrite subUset; apply/andP; split; apply is_invset_Delta. move: {-1}(A :|: B) (erefl (A :|: B)) => /= AUB HAUB AUBD. constructor; rewrite /=. - exact: tclosure_Delta. - exact: tclosureP. - move=> j i k; rewrite /= !inE /= ![~~ _ && _]andbC ![connect _ _ _ && _]andbC. move=> /andP[iltj]; have:= iltj; rewrite ltn_neqAle => /andP[-> _] /= cij. move=> /andP[jltk]; have:= jltk; rewrite ltn_neqAle => /andP[-> _] /= cjk. have iltk := ltn_trans iltj jltk; rewrite iltk /=. have:= iltk; rewrite ltn_neqAle => /andP[-> _] /=. have {cij cjk} /andP := conj cij cjk; apply contraL; rewrite negb_and !negbK. move=> /connectP[/= p Hp Hk] {iltk}. elim: p => [|p0 p IHp] /= in i Hp Hk iltj *. by exfalso; have:= ltn_trans iltj jltk; rewrite Hk ltnn. move: Hp => /andP[ip0AB Hp]; apply /orP. case: (ltngtP p0 j) => [p0ltj | jltp0 | /val_inj Heq]; last 1 first. + by left; apply: connect1; rewrite -Heq. + move/(_ _ Hp Hk p0ltj): IHp => {p Hk Hp} /orP[|->]; last by right. by move/(connect_trans (connect1 (e := srel AUB) ip0AB)); left. + wlog ip0 : A B HAUB isA isB ip0AB / (i, p0) \in A. subst AUB; move=> Hlog; move: ip0AB => /[!inE] /orP[] Hip0. * by have:= Hip0 => {}/(Hlog A B); apply; rewrite //= inE Hip0. * by have:= Hip0 => {}/(Hlog B A); apply; rewrite // setUC // inE Hip0. suffices: ((i, j) \in AUB) || ((j, p0) \in AUB). move/orP=> [ijAB | jp0AB]; [left | right]. * exact: connect1. * by apply/connectP; exists (p0 :: p); rewrite //= jp0AB Hp. rewrite -HAUB !inE -!orbA [((i, j) \in B) || _] orbC -!orbA orbA. apply/or3P; apply Or31; apply/orP. move: isA => [_ _]; rewrite transitive_DeltaI1 => H. have /H/(_ ip0) : i < j < p0 by rewrite iltj jltp0. by move=> [|] -> /=; [left | right]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype