proposition: Lemma lsr_is_even_eq : forall i j, i >> 1 = j >> 1 -> is_even i = is_even j -> i = j.
proof: Proof. intros;apply bit_ext. intros n;destruct (reflect_eqb n 0). rewrite <- (negb_involutive (bit i n)), <- (negb_involutive (bit j n)). rewrite e, <- !is_even_bit, H0;trivial. assert (W1 : [|n|] <> 0%Z) by (intros Heq;apply n0;apply to_Z_inj;trivial). assert (W2 := to_Z_bounded n);clear n0. assert (W3 : [|n-1|] = ([|n|] - 1)%Z). rewrite sub_spec, to_Z_1, Zmod_small;trivial;lia. assert (H1 : n = (n-1)+1). apply to_Z_inj;rewrite add_spec, W3. rewrite Zmod_small;rewrite to_Z_1; lia. case_eq ((n-1) <? digits); intro l. rewrite ltb_spec in l. rewrite H1, <- !bit_half, H; trivial; rewrite ltb_spec; trivial. assert ((digits <=? n) = true). rewrite <- Bool.not_true_iff_false, ltb_spec in l; rewrite leb_spec;lia. rewrite !bit_M;trivial. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz