proposition: Lemma add_list_carry_comm: forall (a b: list bool) (c: bool), add_list_ingr a b c = add_list_ingr b a c.
proof: Proof. intros a. induction a as [ | a' xs IHxs]; intros b c. - simpl. rewrite add_list_ingr_r. reflexivity. - case b as [ | b' ys]. + simpl. auto. + simpl in *. cut (add_carry a' b' c = add_carry b' a' c). * intro H. rewrite H. destruct (add_carry b' a' c) as (r, c0). rewrite IHxs. reflexivity. * case a', b', c; auto. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance