proposition: Lemma filter_list_dec {T} f (ls : list T) : List.length (filter f ls) <= List.length ls.
proof: Proof. induction ls; trivial; simpl in *. repeat match goal with | [ |- context[if ?a then _ else _] ] => destruct a; simpl in * | [ |- S _ <= S _ ] => solve [ apply (fun n m => proj1 (Nat.succ_le_mono n m)); auto ] | [ |- _ <= S _ ] => solve [ apply le_S; auto ] end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common.List.ListFacts