proposition: Lemma pred_count_le_length : forall (A : Type)(P : A -> Prop) ls c, pred_count P ls c -> (c <= length ls)%nat.
proof: Proof. induction ls; intuition; simpl in *. inversion H; subst. trivial. inversion H; clear H; subst. eapply le_n_S. eapply IHls. trivial. econstructor. eapply IHls. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation