proposition: Lemma n_decomp : forall N n m p, 0 < n -> p < (S N) * n -> eqmod n m p -> {k | p = k * n + m}.
proof: Proof. intro N ; induction N ; intros n m p n_pos p_ub p_eqmodn. exists 0 ; inversion p_eqmodn. intuition. rewrite <- H1 in p_ub ; apply False_ind ; intuition lia. case (Compare_dec.le_lt_dec p ((S N) * n)) ; intro p_ub2. case (Compare_dec.le_lt_eq_dec _ _ p_ub2) ; intro H. apply (IHN _ _ _ n_pos H p_eqmodn). rewrite H in p_eqmodn. replace (S N * n) with (N * n + n) in p_eqmodn. destruct (IHN n m (N * n) n_pos) as (k, Hk). apply Nat.mul_lt_mono_pos_r ; [apply n_pos | constructor]. inversion p_eqmodn. apply False_ind. assert (N * n < 0). apply Nat.add_lt_mono_l with n. intuition lia. apply (Nat.nlt_0_r _ H3). replace l with (N * n) in H2. assumption. intuition lia. exists (S k) ; simpl ; rewrite <- Nat.add_assoc ; rewrite <- Hk ; intuition. apply Nat.add_comm. assert (Hrew : p = n + (p - n)). rewrite Nat.add_comm. rewrite Nat.sub_add; [reflexivity|]. apply Nat.le_trans with (S N * n) ; intuition lia; try (apply Nat.le_trans with (S 0 * n) ; intuition ; apply Nat.mul_le_mono_r ; intuition). destruct (IHN n m (p-n) n_pos) as (k, Hk). apply Nat.add_lt_mono_l with n. rewrite <- Hrew ; intuition. rewrite Nat.add_comm in Hrew ; rewrite Hrew in p_eqmodn ; inversion p_eqmodn. apply False_ind ; apply Nat.lt_irrefl with n. apply Nat.lt_trans with (S N * n). intuition lia. apply Nat.lt_trans with p. assumption. rewrite Hrew ; assumption. assert (Hrew' : l = p - n) by intuition lia. rewrite Hrew' in H1 ; assumption. exists (S k) ; simpl ; rewrite <- Nat.add_assoc ; rewrite <- Hk ; intuition. Qed.
imports: PeanoNat NArith Lia