proposition: Lemma add_neg_list_absorb: forall a, add_list a (twos_complement a) = mk_list_false (length a).
proof: Proof. intro a. unfold add_list. rewrite add_neg_list_carry. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance