proposition: Lemma nzhead_app_nzhead d d' : nzhead (app (nzhead d) d') = nzhead (app d d').
proof: Proof. unfold app. rewrite <-(rev_nztail_rev d), rev_rev. generalize (rev d); clear d; intro d. generalize (nzhead_revapp_0 d d'). generalize (nzhead_revapp d d'). generalize (nzhead_revapp_0 (nztail d) d'). generalize (nzhead_revapp (nztail d) d'). rewrite nztail_involutive. now case nztail; [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl) |intros d'' H _ H' _; rewrite H; [rewrite H'|]..]. Qed.
imports: Decimal Arith ZArith