proposition: Lemma bit_ext' : forall a b, (forall n, n <? digits = true -> bit a n = bit b n)%uint63 -> a = b.
proof: Proof. intros. apply bit_ext. intros. assert (digits <=? n = true \/ n <? digits = true)%uint63 by lia. destruct H0. - rewrite! bit_M by auto. reflexivity. - apply H ; auto. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR