proposition: Lemma combine_wplus sz (w1 w2: word sz): #w1 + #w2 < pow2 sz -> forall sz' (w': word sz'), combine (w1 ^+ w2) w' = combine w1 w' ^+ combine w2 ($ 0).
proof: Proof. intros. pre_word_omega. rewrite wordToNat_wplus in *. rewrite ?wordToNat_combine. rewrite wordToNat_natToWord_idempotent' by (apply pow2_zero). rewrite Nat.mul_0_r, Nat.add_0_r. rewrite wordToNat_wplus. rewrite Nat.mod_small by assumption. assert (sth: #w1 + #w2 + pow2 sz * #w' = #w1 + pow2 sz * #w' + #w2) by ring. rewrite <- sth; clear sth. rewrite Nat.mod_small; auto. rewrite Nat.pow_add_r. assert (sth: pow2 sz' = 1 + (pow2 sz' - 1)) by (pose proof (pow2_zero sz'); lia). rewrite sth; clear sth. rewrite Nat.mul_add_distr_l. rewrite Nat.mul_1_r. pose proof (wordToNat_bound w'). pose proof (pow2_zero sz). apply Nat.lt_le_pred in H0. rewrite <-Nat.sub_1_r in H0. pose proof (Nat.mul_le_mono_l _ _ (pow2 sz) H0). 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