proposition: Lemma is_compP s : reflect (forall i, i \in s -> i != 0) (is_comp s).
proof: Proof. rewrite /is_comp; apply (iffP idP) => [H0 i iins|H]. - by move: H0; apply contra => /eqP <-. - by apply/negP => /H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype