proposition: Lemma norm_app_int_norm d d' : unorm d' = zero -> norm (app_int (norm d) d') = norm (app_int d d').
proof: Proof. case d; clear d; intro d; simpl. - now rewrite unorm_app_unorm. - unfold app_int, app. rewrite unorm_0; intro Hd'. rewrite <-rev_nztail_rev. generalize (nzhead_revapp (rev d) d'). generalize (nzhead_revapp_0 (rev d) d'). now case_eq (nztail (rev d)); [intros Hd'' H _; rewrite (H eq_refl); simpl; unfold unorm; simpl; rewrite Hd' |intros d'' Hd'' _ H; rewrite H; clear H; [|now simpl]; set (r := rev _); set (m := match r with Nil => Pos zero | _ => _ end); assert (H' : m = Neg r); [now unfold m; case_eq r; unfold r; [intro H''; generalize (rev_nil_inv _ H'')|..] |rewrite H'; unfold r; clear m r H']; unfold norm; rewrite rev_rev, <-Hd''; rewrite nzhead_revapp; rewrite nztail_involutive; [|rewrite Hd'']..]. Qed.
imports: Decimal Arith ZArith