proposition: Theorem Ndiv_algo_correct : forall n m, n > 0 -> (n | m) -> Ndiv_algo n m=true.
proof: Proof. destruct n. intros. inversion H. intro. pattern m. apply nat_strong_ind. intros. compute. trivial. intros. unfold Ndiv_algo. destruct H1. destruct q. simpl in H1. inversion H1. rewrite Nat.mul_succ_l in H1. rewrite H1. rewrite Ndiv_mod_l1. apply H. apply Nat.le_trans with (q*S n+n). auto with arith. rewrite Nat.add_comm in H1. simpl in H1. apply eq_add_S in H1. rewrite H1. rewrite Nat.add_comm. auto with arith. auto with arith. exists q. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)