proposition: Lemma is_set_decomp : forall k m, is_set k m -> (k = ((k >> (int_of_nat m + 1)) << (int_of_nat m + 1)) lor (1 << int_of_nat m))%uint63.
proof: Proof. intros. apply is_set_eq in H. destruct H as (n & EQ & LT & SET). unfold is_set_int in SET. destruct SET as [F T]. rewrite <- EQ. clear EQ. apply bit_ext. intros. rewrite lor_spec. rewrite ! bit_lsl. rewrite ! bit_lsr. assert (n0 = n \/ n0 <? n = true \/ (Uint63.ltb n n0 && Uint63.ltb n0 digits) = true \/ (Uint63.leb digits n0) = true)%uint63 by lia. destruct H as [H | [H | [H |H]]]. + subst. rewrite T. repeat elim_if. rewrite bit_1. lia. + rewrite F by auto. repeat elim_if. rewrite bit_1. lia. + rewrite andb_true_iff in H. destruct H. replace (n0 <? n + 1)%uint63 with false by lia. simpl. replace (digits <=? n0)%uint63 with false by lia. replace ((n0 - (n + 1) ≤? n + 1 + (n0 - (n + 1)))%uint63) with true by lia. replace ((n + 1 + (n0 - (n + 1))))%uint63 with n0 by lia. elim_if. rewrite bit_1. destruct (bit k n0); lia. + rewrite bit_M; auto. repeat elim_if. rewrite! bit_1. lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR