proposition: Lemma Forall_eq_count_eq_length : forall P l, Forall P l = (count P l = length l).
proof: Proof. Proof using. intros. rewrite LibList.Forall_eq_count_eq_length, length_eq. unfold count. rewrite abs_nonneg; math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)