proposition: Lemma count_card (T : eqType) (x : T) (l : seq T) (P : pred T) : count P l = #|[set i : 'I_(size l) | P (nth x l i)]|.
proof: Proof. elim:l. by move=>/=; apply/esym /eqP; rewrite cards_eq0 -subset0; apply/subsetP=>[[i ilt]]. move=>a l IHl /=. rewrite (cardsD1 (Ordinal (ltn0Sn _))) IHl. rewrite cardsE. have fi: injective (fun i : 'I_(size l)=> lift ord0 i) by move=>[i ilt] [j jlt]/(congr1 val)/=/eqP; rewrite/bump/= 2!add1n eqSS=>/eqP ij; apply val_inj. rewrite -(card_imset _ fi)/=. have/eqP->: [set i : 'I_(size l).+1 | P (nth x (a :: l) i)] :\ Ordinal (ltn0Sn (size l)) == [set lift ord0 i | i in fun x0 : 'I_(size l) => P (nth x l x0)]. rewrite eqEsubset; apply/andP; split; apply/subsetP=>i; rewrite in_setD1 inE. move=>/andP[i0 Pi]. case: (ord_S_split i); last by move=>ie; subst i; move: i0=>/negP; elim. move=>[j ie]; subst i. by apply /imsetP=>/=; exists j. move=>/imsetP/=[j Pj ie]; subst i. by apply/andP; split. by apply/eqP; rewrite eqn_add2r inE; apply/eqP. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries