fact: Definition is_seq (R : nat -> nat -> Prop) c q n := forall i, i < n -> exists y y', is_digit c q i y /\ is_digit c q (1+i) y' /\ R y y'.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)