proposition: Lemma modulus_q_PI:forall xi alpha beta H1 H2, modulus_q xi alpha beta H1 = modulus_q xi alpha beta H2.
proof: Proof. intros xi alpha beta H1. pattern alpha, beta, H1. elim H1 using emits_q_ind_dep; clear H1 xi; [ intros xi alpha0 beta0 i H2; generalize i | intros xi alpha0 beta0 i H2; generalize i | intros xi alpha0 beta0 i H2; generalize i | intros xi alpha0 beta0 f H H2; generalize f H ]; pattern alpha0, beta0, H2; elim H2 using emits_q_ind_dep; first [ intros xi0 alpha' beta' H_primity H_primity'; simpl; case (Incl_T_dec_D xi0 LL); intro; trivial; contradiction | intros xi0 alpha' beta' H_primity H_primity'; simpl; case (Incl_T_dec_D xi0 RR); intro; trivial; contradiction | intros xi0 alpha' beta' H_primity H_primity'; simpl; case (Incl_T_dec_D xi0 MM); intro; trivial; contradiction | intros; contradiction] || (intro xi0; intros; simpl; case (Incl_T_dec_D xi0 LL); intro; contradiction || case (Incl_T_dec_D xi0 RR); intro; contradiction || case (Incl_T_dec_D xi0 MM); intro; contradiction || trivial). Defined.
imports: digits