proposition: Lemma length_add_list_eq: forall (a b: list bool), length a = length b -> length a = length (add_list a b).
proof: Proof. intros a b H. unfold add_list. apply (@add_list_carry_length_eq a b false). exact H. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance