proposition: Lemma filter_length_forallb f (l : list A): length (filter f l) = length l -> forallb f l = true.
proof: Proof. intro H. induction l as [|x l IH]; [reflexivity |]. cbn in *. destruct (f x). - apply IH. now injection H. - exfalso. assert (length l < length (filter f l)) as E. + symmetry in H. apply Nat.eq_le_incl in H. exact H. + eapply Nat.le_ngt; [apply filter_length_le | exact E]. Qed.
imports: PeanoNat