proposition: Lemma modulus_q_PI_strong:forall xi xi' alpha beta alpha' beta' H1 H2, xi=xi'->alpha=alpha' -> beta = beta' -> modulus_q xi alpha beta H1 = modulus_q xi' alpha' beta' H2.
proof: Proof. intros; subst; apply modulus_q_PI. Defined.
imports: digits