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