proposition: Lemma split2_pow2: forall sz n, 2 ^ sz <= n < 2 ^ S sz -> wordToNat (split2 sz 1 (natToWord (sz + 1) n)) = 1.
proof: Proof. intros. rewrite wordToNat_split2. simpl in *. rewrite Nat.add_0_r in *. rewrite wordToNat_natToWord_bound with (bound := wones _). - destruct H. assert (sth: pow2 sz <> 0) by lia. pose proof (Nat.div_le_mono _ _ (pow2 sz) sth H) as sth2. rewrite Nat.div_same in sth2 by auto. apply Nat.lt_le_pred in H0. pose proof (Nat.div_le_mono _ _ (pow2 sz) sth H0) as sth3. rewrite <- Nat.sub_1_r in sth3. assert (sth4: pow2 sz = 1 * pow2 sz) by lia. rewrite sth4 in sth3 at 2. assert (sth5: 1 * pow2 sz + pow2 sz - 1 = 1 * pow2 sz + (pow2 sz - 1)) by lia. rewrite sth5 in sth3. rewrite Nat.div_add_l in sth3 by lia. rewrite Nat.div_small with (a := pow2 sz - 1) in sth3 by lia. lia. - rewrite wones_pow2_minus_one. assert (sth: sz + 1 = S sz) by lia. rewrite sth. simpl. 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