proposition: Lemma rev_intcompn_spec c : is_comp_of_n n (rev c).
proof: Proof. by rewrite /is_comp_of_n /is_comp /= mem_rev sumn_rev; case: c. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype