proposition: Lemma disjoints_prelim : forall n, 0 < n -> forall M m, m < max n M -> {k | k < n /\ eqmod n k m /\ forall l, l <> k -> ~ eqmod n l m}.
proof: Proof. intros n n_pos M ; induction M ; intros m m_ub. rewrite max_l in m_ub ; [| intuition (auto with arith)]. exists m ; repeat split ; [assumption | |]. constructor ; assumption. intros l l_neq Hyp ; apply l_neq ; apply eqmod_uniqueness with (n:=n) (m:=m). intuition. constructor ; assumption. case (Compare_dec.le_lt_dec m (max n M)) ; intro m_ub'. case (Compare_dec.le_lt_eq_dec _ _ m_ub') ; clear m_ub' ; intro m_ub'. apply IHM ; intuition. case (pred_itere _ n_pos m) ; intro Hyp. exists 0 ; apply False_ind ; destruct Hyp as (_,Hf). assert (Hf' : n <= m). apply Nat.le_trans with (max n M) ; [apply Nat.le_max_l | rewrite m_ub' ; intuition]. intuition lia. destruct Hyp as (k,Hk). case (Compare_dec.le_lt_dec k n) ; intro Temp. case (Compare_dec.le_lt_eq_dec _ _ Temp) ; clear Temp ; intro Temp. exists k ; repeat split ; [assumption | |]. rewrite Hk ; constructor ; constructor ; assumption. intros l l_neq eqmodnl ; assert (l_ub := eqmod_bounded _ _ _ eqmodnl) ; apply (eqmod_uniqueness1 _ _ _ l_ub eqmodnl _ Temp). intro Hf ; apply l_neq ; symmetry ; assumption. rewrite Hk ; constructor ; constructor ; assumption. exists 0 ; repeat split. assumption. rewrite Hk ; constructor. replace n with (n+0) in Temp by intuition ; rewrite Temp ; repeat constructor ; assumption. intros l l_neq eqmodnl ; rewrite Hk in eqmodnl. apply l_neq ; apply eqmod_uniqueness2 with (n:=n) (m:=l). apply (eqmod_bounded _ _ _ eqmodnl). assumption. inversion eqmodnl. apply False_ind ; intuition lia. assert (Temp2 := proj1 (Nat.add_cancel_l _ _ _) H) ; replace n with (n+0) in Temp by intuition ; rewrite Temp2, Temp in H1. clear -H1 ; inversion H1. apply False_ind ; intuition lia. repeat (rewrite itere_S in H) ; assert (Temp2 := proj1 (Nat.add_cancel_l _ _ _) H) ; rewrite <- Temp2 ; assumption. constructor. apply (eqmod_bounded _ _ _ eqmodnl). assert (k_ub : k < max n M). rewrite Hk in m_ub' ; intuition lia. destruct (IHM k k_ub) as (p, [p_ub [eqmodnp noteqmodnl]]) ; exists p ; repeat split. assumption. assert (H := eqmod_nS _ _ _ eqmodnp). rewrite Hk ; assumption. intros l l_neq_p eqmodnl. rewrite Hk in eqmodnl ; inversion eqmodnl. clear -H ; intuition lia. repeat (rewrite itere_S in H) ; assert (Temp2 := proj1 (Nat.add_cancel_l _ _ _) H) ; replace n with (n+0) in Temp by intuition. rewrite Temp2 in H1. apply (noteqmodnl _ l_neq_p H1). exists 0 ; apply False_ind. assert (max n M = M). clear -m_ub m_ub' ; induction n. intuition. case (Nat.max_dec (S n) M) ; intro H. rewrite H in m_ub'. case (Nat.max_dec (S n) (S M)) ; intro H'. rewrite H' in m_ub ; apply False_ind ; intuition lia. assert (M < m). apply Nat.le_lt_trans with (max (S n) M). apply Nat.le_max_r. rewrite H ; assumption. rewrite H' in m_ub. apply False_ind ; intuition lia. assumption. assert (m < max (S n) (S M)). apply Nat.lt_le_trans with (max n (S M)). assumption. generalize M ; clear ; induction n. intuition. intro M ; replace (max (S (S n)) (S M)) with (S (max (S n) M)) by intuition. replace (max (S n) (S M)) with (S (max n M)) by intuition. apply (proj1 (Nat.succ_le_mono _ _)). destruct M. repeat (rewrite Nat.max_comm ; simpl); intuition. apply IHn. simpl in H0. intuition lia. Qed.
imports: PeanoNat NArith Lia