proposition: Lemma add_list_assoc: forall (a b c: list bool), (add_list (add_list a b) c) = (add_list a (add_list b c)).
proof: Proof. intros a b c. unfold add_list. apply (@add_list_carry_assoc a b c false false false false). simpl; reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance