proposition: Lemma not_list_true_false: forall n, map negb (mk_list_true n) = mk_list_false n.
proof: Proof. intro n. induction n as [ | n IHn]. - auto. - simpl. apply f_equal. exact IHn. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance