proposition: Lemma cardD1x (I : finType) (A : pred I) j : A j -> #|SimplPred A| = 1 + #|[pred i | A i & i != j]|.
proof: Proof. move=> Aj; rewrite (cardD1 j) [j \in A]Aj; congr (_ + _). by apply: eq_card => i; rewrite inE /= andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)