proposition: Lemma coPrimeSeq : forall c i j n : nat, divide (factorial n) c -> i <> j -> i <= n -> j <= n -> CoPrime (coPrimeBeta i c) (coPrimeBeta j c).
proof: Proof. unfold coPrimeBeta in |- *. intros ? ? ? ? H H0 H1 H2. rewrite Nat.lt_gt_cases in H0; destruct H0 as [H3 | H3]. - eapply coPrimeSeqHelp. apply H. assumption. assumption. assumption. - apply coPrimeSym. eapply coPrimeSeqHelp. + apply H. + assumption. + assumption. + assumption. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow