proposition: Lemma inord_predS (i : 'I_n) a b : a < i -> i < b -> (inord (n' := n0) i.-1).+1 < b.
proof: Proof. Proof using. move=> Ha Hb; rewrite inordK; last by apply (leq_ltn_trans (leq_pred _)). by rewrite (ltn_predK Ha). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr