fact: Definition set_digit x p (b:bool) := if if 0 <=? p then p <? digits else false then if b then x lor (1 << p) else x land (max_int lxor (1 << p)) else x.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63