proposition: Lemma eq_inv_allgt_imply 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=> H; have:= eq_inv_size H. move: H; rewrite /eq_inv /versions => H /= /eqP; rewrite eqSS => /eqP Hsz. move/(all_nthP inh) => Hall; apply/(all_nthP inh). rewrite -Hsz => i Hi; move/(_ i Hi) : Hall => Hleq. move/(_ 0 i.+1) : H => /=. move: Hi; rewrite -Hsz -ltnS => -> /=. by rewrite ltNge => <-; rewrite -ltNge. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp