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