proposition: Theorem Ndiv_algo_complete : forall n m, n>0 -> Ndiv_algo n m=true -> (n | m).
proof: Proof. intros. unfold Ndiv_algo in H0. apply Nat.eqb_eq in H0. replace m with (m-0). apply Ndiv_mod_algo_complete. auto. auto. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)