proposition: Lemma add_list_carry_length_eq: forall (a b: list bool) c, length a = length b -> length a = length (add_list_ingr a b c).
proof: Proof. induction a as [ | a' xs IHxs]. simpl. auto. intros [ | b ys]. - simpl. intros. exact H. - intros. simpl in *. case_eq (add_carry a' b c); intros r c0 Heq. simpl. apply f_equal. specialize (@IHxs ys). apply IHxs. inversion H; reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance