proposition: Lemma sext_natToWord': forall sz1 sz2 n, (2 * n < pow2 sz1)%nat -> sext (natToWord sz1 n) sz2 = natToWord (sz1 + sz2) n.
proof: Proof. induction sz1; intros. - simpl. unfold sext. simpl. unfold wzero. unfold pow2 in *. assert (n=0) by lia. subst n. reflexivity. - unfold sext in *. assert (@wmsb (S sz1) (natToWord (S sz1) n) false = false) as E by (apply wmsb_0_natToWord; assumption). rewrite E. clear E. simpl. unfold natToWord. f_equal. fold natToWord. specialize (IHsz1 sz2 (Nat.div2 n)). rewrite <- IHsz1. + assert (@wmsb sz1 (natToWord sz1 (Nat.div2 n)) false = false) as E. { destruct sz1. - reflexivity. - apply wmsb_0_natToWord. unfold pow2 in *. fold pow2 in *. assert ((2 * Nat.div2 n <= n)%nat) by apply two_times_div2_bound. lia. } rewrite E. clear E. reflexivity. + replace (pow2 (S sz1)) with (2 * (pow2 sz1)) in H. * assert ((2 * Nat.div2 n <= n)%nat) by apply two_times_div2_bound. lia. * 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