proposition: Lemma coPrimeSeqHelp : forall c i j n : nat, divide (factorial n) c -> i < j -> i <= n -> j <= n -> CoPrime (S (c * S i)) (S (c * S j)).
proof: Proof. intros ? ? ? ? H H0 H1 H2. apply coPrimePrime. intros p H3. destruct (divdec (S (c * S i)) p) as [H4 | H4]. assert (H5: ~ divide p c). { intro H5. assert (H6: divide p 1). { eapply div_plus_r. apply div_mult_compat_l. apply H5. rewrite Nat.add_comm. simpl in |- *. apply H4. } induction H3 as (H3, H7). red in H3; rewrite Nat.lt_nge in H3; apply H3. destruct H6 as [x Hx];destruct x; lia. } destruct (divdec (S (c * S j)) p). assert (H7: divide p (c * (j - i))). { rewrite minusS. rewrite Nat.mul_comm. rewrite Nat.mul_sub_distr_r. rewrite (Nat.mul_comm (S j)). rewrite (Nat.mul_comm (S i)). rewrite minusS. destruct H4, H6. rewrite H4, H6. exists (x0 - x). nia. } destruct (primedivmult _ _ _ H3 H7). - elim H5. assumption. - assert (H9: j - i <= n). { eapply Nat.le_trans. apply Nat.le_sub_l. assumption. } elim H5. apply div_trans with (factorial n). apply div_trans with (j - i). assumption. unfold factorial in |- *. assert (H10: 1 <= j - i). { assert (H10: j = i + (j - i)). rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity. apply Nat.lt_le_incl; assumption. rewrite H10 in H0; lia. } replace (j - i) with (S (pred (j - i))). apply divProd. rewrite <- Nat.sub_1_r. apply Nat.succ_lt_mono. apply Nat.lt_succ_r. replace (S (j - i - 1)) with (1 + (j - i - 1)). rewrite Nat.add_comm, Nat.sub_add. assumption. assumption. auto. induction (j - i). elim (Nat.nle_succ_diag_l _ H10). rewrite <- pred_Sn. reflexivity. assumption. - auto. - auto. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow