proposition: Lemma add_list_carry_assoc: forall (a b c: list bool) (d1 d2 d3 d4: bool), add_carry d1 d2 false = add_carry d3 d4 false -> (add_list_ingr (add_list_ingr a b d1) c d2) = (add_list_ingr a (add_list_ingr b c d3) d4).
proof: Proof. intros a. induction a as [ | a' xs IHxs]; intros b c d1 d2 d3 d4. - simpl. reflexivity. - case b as [ | b' ys]. + simpl. auto. + case c as [ | c' zs]. * simpl. rewrite add_list_ingr_r. auto. * simpl. case_eq (add_carry a' b' d1); intros r0 c0 Heq0. simpl. case_eq (add_carry r0 c' d2); intros r1 c1 Heq1. case_eq (add_carry b' c' d3); intros r3 c3 Heq3. case_eq (add_carry a' r3 d4); intros r2 c2 Heq2. intro H. rewrite (IHxs _ _ c0 c1 c3 c2); revert Heq0 Heq1 Heq3 Heq2; case a', b', c', d1, d2, d3, d4; simpl; do 4 (intros H'; inversion_clear H'); try reflexivity; simpl in H; discriminate. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance