proposition: Lemma add_list_carry_twice: forall a c, add_list_ingr a a c = removelast (c :: a).
proof: Proof. intro a. induction a as [ | a xs IHxs]. - intros c. simpl. reflexivity. - intros [ | ]. + simpl. case a. * simpl. rewrite IHxs. case_eq xs. intro Heq0. simpl. reflexivity. reflexivity. * simpl. rewrite IHxs. case_eq xs. intro Heq0. simpl. reflexivity. reflexivity. + simpl. case a. * simpl. rewrite IHxs. case_eq xs. intro Heq0. simpl. reflexivity. reflexivity. * simpl. rewrite IHxs. case_eq xs. intro Heq0. simpl. reflexivity. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance