proposition: Lemma split_all : forall i m, i = split_m i m.
proof: Proof. intros. unfold split_m. apply bit_ext. intros. rewrite lor_spec. rewrite Uint63.land_spec. rewrite bit_lsl. rewrite Uint63.land_spec. rewrite! bit_ones. generalize (bit_M i n). destruct ((n <? m)%uint63 || (digits ≤? n)%uint63) eqn:T1. destruct ((n <? m)%uint63 && (n <? 63)%uint63) eqn:T2. - unfold digits in *. destruct (bit i n); try lia. - unfold digits in *. destruct (bit i n); try lia. - destruct ((n - m <? digits)%uint63 && (n - m <? 63)%uint63) eqn:T2. destruct ((n <? m)%uint63 && (n <? 63)%uint63) eqn:T3. unfold digits in *. destruct (bit i n); try lia. unfold digits in *. destruct (bit i n); try lia. destruct ((n <? m)%uint63 && (n <? 63)%uint63) eqn:T3. unfold digits in *. destruct (bit i n); try lia. unfold digits in *. destruct (bit i n); try lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR