proposition: Lemma sext_wplus_wordToZ_distr: forall sz (w1 w2: word sz) n, n <> 0 -> wordToZ (sext w1 n ^+ sext w2 n) = (wordToZ (sext w1 n) + wordToZ (sext w2 n))%Z.
proof: Proof. intros. destruct n; [exfalso; auto|clear H]. apply eq_sym, wordToZ_wplus_bound'; [lia|]. do 2 rewrite sext_wordToZ. destruct sz. - rewrite (shatter_word w1), (shatter_word w2). cbn; split; try (pose proof (pow2_zero n); lia). - replace (pred (S sz + S n)) with (S (sz + n)) by lia. pose proof (wordToZ_size' w1); destruct H. pose proof (wordToZ_size' w2); destruct H1. split. + rewrite pow2_S_z. etransitivity; [|eapply Z.add_le_mono; eassumption]. rewrite <-Z.add_diag, Z.opp_add_distr. apply Z.add_le_mono; rewrite <-Z.opp_le_mono; apply Nat2Z.inj_le, pow2_le; lia. + rewrite pow2_S_z. eapply Z.lt_le_trans; [eapply Z.add_lt_mono; eassumption|]. rewrite <-Z.add_diag. apply Z.add_le_mono; apply Nat2Z.inj_le, pow2_le; lia. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.Equivalence Coq.Arith.PeanoNat Coq.ZArith.BinInt  Coq.Arith.Arith Coq.NArith.NArith Coq.Bool.Bool Coq.ZArith.ZArith Coq.Logic.Eqdep_dec Coq.Logic.EqdepFacts Coq.Program.Tactics Coq.Program.Equality Coq.setoid_ring.Ring Coq.setoid_ring.Ring_polynom bbv.Nomega bbv.ZLib bbv.NatLib bbv.NLib bbv.N_Z_nat_conversions bbv.DepEq bbv.DepEqNat bbv.ReservedNotations Coq.micromega.Lia