proposition: Lemma add_neg_list_carry: forall a, add_list_ingr a (twos_complement a) false = mk_list_false (length a).
proof: Proof. intro a. induction a as [ | a xs IHxs]. - simpl. reflexivity. - unfold twos_complement. rewrite add_neg_list_carry_false. rewrite not_list_length at 1. rewrite add_list_carry_empty_neutral_r. rewrite add_neg_list_carry_neg_t. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance