proposition: Lemma eq_inv_allgtnX d1 d2 (S : inhOrderType d1) (T : inhOrderType d2) (a : S) u (b : T) v : eq_inv (a :: u) (b :: v) -> (allLtn u a) = (allLtn v b).
proof: Proof. move=> H1; have H2 := eq_inv_sym H1. by apply/idP/idP; apply: eq_inv_allgt_imply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp