proposition: Lemma intcompn2 (sh : intcompn 2) : sh = [:: 2] :> seq nat \/ sh = [:: 1; 1] :> seq nat.
proof: Proof. case: sh => sh Hsh /=; move: Hsh; rewrite enum_compnP. by rewrite /enum_compn /= !inE => /orP[] /eqP ->; [right | left]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype