proposition: Lemma N_pos_div_eucl_q0 : forall i b r, N.pos_div_eucl i (N.pos b) = (0%N, r) -> i = N2pos r.
proof: Proof. intros i b r H; generalize (N.pos_div_eucl_spec i (N.pos b)). rewrite H. simpl. destruct r. discriminate. injection 1;now cbn. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)