proposition: Theorem wbit_and_not_other: forall sz sz' (n1 n2 : word sz'), (wordToNat n1 < sz)%nat -> (wordToNat n2 < sz)%nat -> n1 <> n2 -> (wbit sz n1) ^& wnot (wbit sz n2) = wbit sz n1.
proof: Proof. induction sz; intros; try lia. unfold wbit, wzero, wand, wnot. simpl. destruct (zero_or_wordToNat_S n1); destruct (zero_or_wordToNat_S n2); try congruence; destruct_conjs; subst; fold wnot; try rewrite roundTrip_0; simpl; f_equal. rewrite H4; simpl; rewrite mod2_pow2_twice; auto. rewrite H4; simpl; rewrite div2_pow2_twice; apply wand_kill. rewrite H4; simpl; rewrite mod2_pow2_twice; auto. rewrite H4; simpl; rewrite div2_pow2_twice. rewrite wnot_zero. rewrite wand_comm. apply wand_unit. rewrite H4; simpl; rewrite mod2_pow2_twice; simpl; apply andb_true_r. rewrite H4; rewrite H6; simpl. repeat rewrite div2_pow2_twice. apply IHsz; try lia. apply word_neq. unfold not in *; intros; apply H1. apply sub_0_eq. rewrite <- H2. ring_sz sz'. 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