proposition: Lemma BZ_i0P x: intp x <-> (inc x BZms \/ inc x BZp).
proof: Proof. split; last by case => h; [apply:BZms_sBZ | apply:BZp_sBZ]. move /candu2P => [pa] [] [pb pc]. + by left; rewrite -pa pc; apply: indexed_pi. + by right;rewrite -pa pc; apply: indexed_pi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)