proposition: Lemma coPrimeProd : forall (n : nat) (x : nat -> nat), (forall z1 z2 : nat, z1 < S n -> z2 < S n -> z1 <> z2 -> CoPrime (x z1) (x z2)) -> (forall z : nat, z < S n -> x z > 0) -> CoPrime (prod n x) (x n).
proof: Proof. induction n as [| n Hrecn]. - intros; simpl in |- *; apply coPrime1. - intros x H H0. assert (H1: forall z1 z2 : nat, z1 < S n -> z2 < S n -> z1 <> z2 -> CoPrime (x z1) (x z2)). { intros;apply H. 1,2: now apply Nat.lt_lt_succ_r. - assumption. } simpl in |- *; apply coPrimeMult3. + apply H0. apply Nat.lt_lt_succ_r. apply Nat.lt_succ_diag_r. + apply prodBig1. intros; apply H0. do 2 apply Nat.lt_lt_succ_r. assumption. + apply H0. apply Nat.lt_succ_diag_r. + apply H. apply Nat.lt_lt_succ_r. apply Nat.lt_succ_diag_r. apply Nat.lt_succ_diag_r. auto. + set (A1 := fun a : nat => match eq_nat_dec a n with | left _ => x (S n) | right _ => x a end) in *. assert (H2: CoPrime (prod n A1) (A1 n)). { apply Hrecn. intros. unfold A1 in |- *. induction (eq_nat_dec z1 n). + induction (eq_nat_dec z2 n). * elim H4. rewrite a0. assumption. * apply H. apply Nat.lt_succ_diag_r. apply Nat.lt_lt_succ_r. assumption. unfold not in |- *; intros. rewrite H5 in H3. elim (Nat.lt_irrefl _ H3). + induction (eq_nat_dec z2 n). * apply H. apply Nat.lt_lt_succ_r. assumption. apply Nat.lt_succ_diag_r. unfold not in |- *; intros. rewrite H5 in H2. elim (Nat.lt_irrefl _ H2). * apply H. apply Nat.lt_lt_succ_r. assumption. apply Nat.lt_lt_succ_r. assumption. assumption. + intros. unfold A1 in |- *. induction (eq_nat_dec z n). * apply H0. apply Nat.lt_succ_diag_r. * apply H0. apply Nat.lt_lt_succ_r. assumption. } auto. replace (x (S n)) with (A1 n). replace (prod n x) with (prod n A1). assumption. apply prodExtensional. intros. unfold A1 in |- *. induction (eq_nat_dec z n). * rewrite a in H3. elim (Nat.lt_irrefl _ H3). * reflexivity. * unfold A1 in |- *. induction (eq_nat_dec n n). -- reflexivity. -- elim b; reflexivity. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow