proposition: Lemma countb_false l : countb false l = length l - countb true l.
proof: Proof. cut (countb false l + countb true l = length l). lia. induction l as [| [|] l IHl]; simpl; lia. Qed.
imports: Arith ZArith String List Psatz Factorial