proposition: Lemma is_comp_cons i s : is_comp (i :: s) = (i != 0) && (is_comp s).
proof: Proof. by rewrite /is_comp inE negb_or eq_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype