proposition: Lemma countLeadingZerosWord_lt_len no ni: ni < pow2 no -> forall w: word ni, w <> wzero ni -> (countLeadingZerosWord no w < natToWord _ ni)%word.
proof: Proof. induction ni; auto; intros. - shatter_word w. tauto. - unfold countLeadingZerosWord; fold countLeadingZerosWord. rewrite nat_cast_cast. match goal with | |- ((if ?P then _ else _) < _)%word => destruct P; simpl; auto end. + 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. } apply wordToNat_zero in e. match type of IHni with | split1 ni 1 ?P <> _ -> _ => assert (sth3: #P <> 0) by (rewrite <- wordToNat_cast; auto); apply wordToNat_notZero in sth3; rewrite <- (combine_split ni 1 P) in sth3 end. rewrite e in *. match type of sth3 with | combine ?P _ <> _ => destruct (weq P (natToWord _ 0)); [rewrite e0 in *; rewrite combine_zero in sth3; tauto|] end. specialize (IHni n). rewrite <- ?(@natplus1_wordplus1_eq _ _ (wones no)); auto. * pre_word_omega. lia. * 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. + pre_word_omega. rewrite wordToNat_natToWord_idempotent'; auto; try 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