proposition: Fact is_digit_fun c q i x y : is_digit c q i x -> is_digit c q i y -> x = y.
proof: Proof. intros (H1 & a1 & b1 & H3 & H4) (H2 & a2 & b2 & H5 & H6). rewrite H3 in H5. apply div_rem_uniq, proj1 in H5; auto; try lia. apply div_rem_uniq, proj2 in H5; auto; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)