proposition: Lemma length_twos_complement: forall (a: list bool), length a = length (twos_complement a).
proof: Proof. intro a. induction a as [ | a' xs IHxs]. - auto. - unfold twos_complement. specialize (@add_list_carry_length_eq (map negb (a' :: xs)) (mk_list_false (length (a' :: xs))) true). intro H. rewrite <- H. simpl. apply f_equal. rewrite <- not_list_length. reflexivity. rewrite length_mk_list_false. rewrite <- not_list_length. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance