proposition: Theorem betaTheorem1 : forall (n : nat) (y : nat -> nat), {a : nat * nat | forall z : nat, z < n -> y z = snd (proj1_sig (div_eucl (coPrimeBeta z (snd a)) (gtBeta z (snd a)) (fst a)))}.
proof: Proof. intros n y. unfold beta. set (c := factorial (max n (maxBeta n y))) in *. set (x := fun z : nat => coPrimeBeta z c) in *. assert (H: forall z1 z2 : nat, z1 < n -> z2 < n -> z1 <> z2 -> CoPrime (x z1) (x z2)). { intros; unfold x in |- *; eapply coPrimeSeq. - eapply div_trans. + unfold factorial in |- *; apply divProd2. apply Nat.le_max_l. + unfold c, factorial in |- *. exists 1; now rewrite Nat.mul_1_r. - assumption. - now apply Nat.lt_le_incl. - apply Nat.lt_le_incl; assumption. } assert (H0: forall z : nat, z < n -> y z < x z). { intros; unfold x, coPrimeBeta in |- *. apply Nat.lt_succ_r. induction (mult_O_le c (S z)). - discriminate H1. - apply Nat.le_trans with c. + unfold c in |- *. apply Nat.le_trans with (max n (maxBeta n y)). apply Nat.le_trans with (maxBeta n y). apply maxBetaLe. assumption. apply Nat.le_max_r. generalize (max n (maxBeta n y)). intros. induction n0 as [| n0 Hrecn0]. simpl in |- *. apply Nat.le_succ_diag_r. induction n0 as [| n0 Hrecn1]. simpl in |- *. apply le_n. assert (H2: factorial n0 > 0). { unfold factorial in |- *. apply prodBig1. intros. apply Nat.lt_0_succ. } simpl in |- *. apply Nat.le_trans with (1 + (1 + n0 * (factorial n0 + n0 * factorial n0))). * simpl in |- *. repeat apply le_n_S. induction (mult_O_le n0 (factorial n0 + n0 * factorial n0)). -- unfold gt in H2. assert (H4: factorial n0 = factorial n0 + 0) by (rewrite Nat.add_comm; auto). rewrite H4 in H2. set (A1 := factorial n0 + 0) in *. rewrite <- H3 in H2. unfold A1 in H2. clear H4 A1. assert (H4: n0 * factorial n0 < 0). { eapply Nat.add_lt_mono_l. apply H2. } elim (Nat.nlt_0_r _ H4). -- rewrite Nat.mul_comm; assumption. * apply Nat.add_le_mono. apply le_plus_trans. apply Nat.lt_succ_r. rewrite <- Nat.succ_lt_mono. auto. apply Nat.add_le_mono. apply le_plus_trans. apply Nat.lt_succ_r. rewrite <- Nat.succ_lt_mono. assumption. apply le_n. + now rewrite Nat.mul_comm. } destruct (chRem _ _ H _ H0) as [x0 [H2 H3]]. exists (x0, c). intros z H1; rewrite (H3 z H1). induction (div_eucl (x z) (ltgt1 (y z) (x z) (H0 z H1)) x0). simpl fst; simpl snd. destruct (div_eucl (coPrimeBeta z c) (gtBeta z c) x0) as [x2 p0]. simpl in |- *. eapply uniqueRem. apply gtBeta. unfold x in p. exists (fst x1); apply p. exists (fst x2); apply p0. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow