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