proposition: Lemma mask_small : forall m n (BOUND : n < 63) (BITN : is_mask m n), m = Uint63.lsl one (int_of_nat n).
proof: Proof. unfold one. intros. apply testbit_spec. intros. destruct (testbit m n0) eqn:TEST. - assert (n = n0). { apply BITN;auto. } subst. clear BITN. unfold testbit in *. revert TEST. rewrite Uint63.bit_lsl. rewrite bit_1. repeat elim_if. lia. - assert (n <> n0). { specialize (BITN n0). intuition congruence. } unfold testbit. rewrite Uint63.bit_lsl. rewrite bit_1. repeat elim_if ; intuition try lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR