proposition: Lemma split1_combine_wplus sz1 sz2 (w11 w21: word sz1) (w12 w22: word sz2): split1 _ _ (combine w11 w12 ^+ combine w21 w22) = w11 ^+ w21.
proof: Proof. rewrite <- natToWord_wordToNat at 1. rewrite wordToNat_split1. rewrite <- wordToNat_plus. rewrite ?wordToNat_combine. assert (sth: #w11 + pow2 sz1 * #w12 + (#w21 + pow2 sz1 * #w22) = #w11 + #w21 + pow2 sz1 * (#w12 + #w22)) by ring. rewrite wordToNat_natToWord_eqn. rewrite sth. rewrite Nat.pow_add_r. assert (pow2 sz1 <> 0) by (pose proof (pow2_zero sz1); intro; lia). assert (pow2 sz2 <> 0) by (pose proof (pow2_zero sz2); intro; lia). rewrite mod_factor by auto. rewrite Nat.add_mod by auto. assert (sth2: pow2 sz1 * (# w12 + #w22) = (#w12 + #w22) * pow2 sz1) by ring. rewrite sth2. rewrite Nat.mod_mul by auto. rewrite Nat.add_0_r. rewrite Nat.mod_mod by auto. rewrite <- wordToNat_natToWord_eqn. rewrite natToWord_wordToNat. rewrite natToWord_plus. rewrite ?natToWord_wordToNat. auto. 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