proposition: Lemma wordToNat_split1: forall sz1 sz2 (w: word (sz1 + sz2)), wordToNat (split1 _ _ w) = Nat.modulo (wordToNat w) (pow2 sz1).
proof: Proof. induction sz1; intros; [reflexivity|]. destruct (destruct_word_S w) as [v [b E]]. match type of v with | word ?x => change x with (sz1 + sz2) in * end. subst w. rename v into w. simpl; rewrite IHsz1. pose proof (zero_lt_pow2 sz1). destruct b. - change (pow2 sz1 + (pow2 sz1 + 0)) with (2 * pow2 sz1). replace (S (wordToNat w * 2)) with (1 + 2 * wordToNat w) by lia. rewrite Nat.add_mod by lia. rewrite Nat.mul_mod_distr_l; [|lia|discriminate]. rewrite Nat.mod_1_l by lia. rewrite Nat.mul_comm with (n:= 2). change (1 + wordToNat w mod pow2 sz1 * 2) with (S (wordToNat w mod pow2 sz1 * 2)). apply eq_sym, Nat.mod_small. assert (pow2 sz1 <> 0) by lia. pose proof (Nat.mod_upper_bound (wordToNat w) (pow2 sz1) H0). lia. - change (pow2 sz1 + (pow2 sz1 + 0)) with (2 * pow2 sz1). rewrite Nat.mul_comm with (n:= 2). rewrite Nat.mul_mod_distr_r; [|lia|discriminate]. reflexivity. 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