proposition: Theorem Ndiv_mod_algo_complete : forall n m r, n > 0 -> Ndiv_mod_algo n m = r -> (n | m - r).
proof: Proof. destruct n. + intros; inversion H. + intro m; pattern m; apply nat_strong_ind. - intros; compute in H0; rewrite <- H0. simpl; apply Ndiv_0. - intros; simpl in H1; case (lt_eq_lt_dec (S n) n0). intros; destruct s. { assert (exists d, n0=S n+d) by (apply Nle_plus; auto with arith). destruct H2; rewrite H2 in H1. assert (Ndiv_mod_algo (S n) (S n+x)=Ndiv_mod_algo (S n) (x+S n)) by (rewrite Nat.add_comm; auto). rewrite H3 in H1. clear H3. rewrite Ndiv_mod_l1 in H1. rewrite H2. replace (S (S n+x)) with (S n+S x) by auto with arith. replace (S n+S x-r) with (S n+(S x-r)). 2: { symmetry. apply Nat.add_sub_eq_l. replace (r+(S n+(S x-r))) with (S n+r+(S x-r)). 2: { rewrite Nat.add_assoc. now auto with arith. } assert (S x=r+(S x-r)). symmetry. rewrite Nat.add_comm. apply Nat.sub_add. destruct (Nat.eqb n (Ndiv_mod_algo (S n) x)). rewrite <- H1. auto with arith. destruct r. inversion H1. apply eq_add_S in H1. apply le_n_S. apply Ndiv_mod_algo_rem2 with (S n). auto with arith. auto. rewrite H3. rewrite Nat.add_assoc. rewrite (Nat.add_comm r). rewrite Nat.add_sub. auto. } apply Ndiv_plus_compat. apply Ndiv_n_n. apply H. rewrite Nat.add_succ_comm in H2. apply Nat.le_trans with (S x+n). auto with arith. rewrite Nat.add_comm. rewrite <- H2. auto with arith. auto with arith. auto. auto with arith. } { rewrite <- e in H1. replace (Ndiv_mod_algo (S n) (S n)) with (Ndiv_mod_algo (S n) (0+S n)) in H1. rewrite Ndiv_mod_l1 in H1. simpl in H1; destruct n. { simpl in H1; rewrite <- H1; rewrite <- e; simpl; exists 2; ring. } { simpl in H1; rewrite <- H1; rewrite e; simpl; rewrite Nat.sub_0_r; apply Ndiv_n_n. } { auto with arith. } { simpl. auto. } } { intro; replace (Ndiv_mod_algo (S n) n0) with n0 in H1. apply le_le_S_eq in l. destruct l. assert (n<>n0). intro. rewrite H3 in H2. apply Nat.lt_irrefl in H2. auto. apply eq_nat_correct in H3. rewrite <- H3 in H1. rewrite <- H1. rewrite Nat.sub_diag. apply Ndiv_0. apply eq_add_S in H2. rewrite H2 in H1. rewrite Nat.eqb_refl in H1. rewrite <- H1. rewrite <- Nat.sub_0_r. rewrite H2. apply Ndiv_n_n. symmetry. apply Ndiv_mod_l0. auto. } Qed.
imports: Coq(Arith Euclid Compare Lia)