proposition: Theorem hd_filter_false_eq_and_false : forall (A : Type)(ls : list A)(P : A -> bool), (if hd_error (filter P ls) then false else true) = fold_left (fun (b : bool) (z : A) => b && negb (P z)) ls true.
proof: Proof. induction ls; intuition; simpl in *. destruct (P a). simpl. rewrite fold_and_false_init. trivial. eapply IHls. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation