proposition: Lemma pred_count_listRepeat_ne_inv : forall n (A : Type)(a1 a2 : A) count, a1 <> a2 -> pred_count (eq a1) (listRepeat a2 n) count -> count = O.
proof: Proof. induction n; intuition; simpl in *. inversion H0. trivial. inversion H0; clear H0; subst. intuition. eapply IHn; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation