proposition: Lemma wordToNat_split2: forall sz1 sz2 (w: word (sz1 + sz2)), wordToNat (split2 _ _ w) = Nat.div (wordToNat w) (pow2 sz1).
proof: Proof. induction sz1; intros; [rewrite Nat.div_1_r; 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. change (split2 (S sz1) sz2 (WS b w)) with (split2 sz1 sz2 w). rewrite IHsz1. destruct b. - unfold pow2; fold pow2. replace (@wordToNat (S sz1 + sz2) w~1) with (1 + 2 * wordToNat w) by (simpl; lia). rewrite <-Nat.div_div; [|discriminate|pose proof (zero_lt_pow2 sz1); lia]. rewrite Nat.mul_comm, Nat.div_add by discriminate. rewrite Nat.div_small with (b := 2) by lia. reflexivity. - unfold pow2; fold pow2. replace (@wordToNat (S sz1 + sz2) w~0) with (2 * wordToNat w) by (simpl; lia). rewrite Nat.div_mul_cancel_l; [|pose proof (zero_lt_pow2 sz1); 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