proposition: Lemma Dade_support1_TI : {in A &, forall a b, ~~ [disjoint dd1 a & dd1 b] -> exists2 x, x \in L & b = a ^ x}.
proof: Proof. move=> a b Aa Ab /= /pred0Pn[_ /andP[/imset2P[x u /(piHA Aa) def_x Gu ->]]] /=. case/imset2P=> y v /(piHA Ab) def_y Gv /(canLR (conjgK v)) def_xuv. have def_b: a ^ (u * v^-1) = b by rewrite -def_x -consttJ conjgM def_xuv def_y. by apply/imsetP/conjAG; rewrite // -def_b imset_f ?groupM ?groupV. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius ssrnum) mathcomp(matrix mxalgebra mxrepresentation vector algC classfun character) mathcomp(inertia vcharacter) odd_order(PFsection1)