proposition: Lemma add_list_comm: forall (a b: list bool), (add_list a b) = (add_list b a).
proof: Proof. intros a b. unfold add_list. apply (add_list_carry_comm a b false). Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance