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