proposition: Lemma is_partition_with_complement x j: sub j x -> partition_w_fam (partition_with_complement x j) x.
proof: Proof. rewrite /partition_with_complement=> jx; split. - by apply: variantLc_fgraph. - move=> a b; aw;case /C2_P => -> ;case /C2_P => ->; fprops; right; aw; [ | apply (disjoint_S)];apply:set_I2Cr. - by rewrite/unionb /variantLc variant_d setUf2f; aw; apply:setU2_Cr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)