proposition: Lemma inordi_neq_i1 n i : i < n -> (@inord n i != @inord n i.+1).
proof: Proof. move=> Hi. rewrite /eq_op /= inordK; last by apply (leq_trans Hi). rewrite inordK; last exact: Hi. by rewrite ieqi1F. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr