proposition: Lemma countLeadingZerosWord_le_len no ni: ni < pow2 no -> forall w: word ni, (countLeadingZerosWord no w <= natToWord _ ni)%word.
proof: Proof. induction ni; simpl; auto; intros. - word_lia. - match goal with | |- ((if ?P then _ else _) <= _)%word => destruct P; simpl; auto end; [| word_lia]. assert (sth: ni < pow2 no) by lia. specialize (IHni sth). assert (sth1: natToWord no (S ni) = natToWord no (1 + ni)) by auto. rewrite sth1. rewrite natToWord_plus. match goal with | |- ((_ ^+ countLeadingZerosWord no ?P) <= _)%word => specialize (IHni P) end. match goal with | |- (?a ^+ ?b <= ?c ^+ ?d)%word => rewrite (wplus_comm a b); rewrite (wplus_comm c d) end. pre_word_omega. assert (sth2: no > 0). { destruct no; [|lia]. destruct ni; simpl in *; try lia. } rewrite <- ?(@natplus1_wordplus1_eq _ _ (wones no)); auto. + pre_word_omega. rewrite wordToNat_natToWord_eqn. rewrite Nat.mod_small; auto. + pre_word_omega. rewrite wordToNat_natToWord_eqn in IHni. rewrite Nat.mod_small in IHni; 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